From af5f3e4ec6cec96b996485fd0cf3825cdde9b712 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Wed, 14 Oct 2026 21:41:29 +0200 Subject: [PATCH 1/2] Add differential privacy theory and Gaussian rdo programs --- README.md | 110 +++++- RandomDo.lean | 1 + RandomDo/DifferentialPrivacy.lean | 13 + RandomDo/DifferentialPrivacy/Basic.lean | 129 +++++++ RandomDo/DifferentialPrivacy/Calibration.lean | 167 +++++++++ RandomDo/DifferentialPrivacy/Dataset.lean | 86 +++++ RandomDo/DifferentialPrivacy/Gaussian.lean | 316 ++++++++++++++++++ RandomDo/DifferentialPrivacy/Mean.lean | 144 ++++++++ RandomDo/DifferentialPrivacy/Programs.lean | 258 ++++++++++++++ Test.lean | 1 + Test/DifferentialPrivacy.lean | 150 +++++++++ 11 files changed, 1374 insertions(+), 1 deletion(-) create mode 100644 RandomDo/DifferentialPrivacy.lean create mode 100644 RandomDo/DifferentialPrivacy/Basic.lean create mode 100644 RandomDo/DifferentialPrivacy/Calibration.lean create mode 100644 RandomDo/DifferentialPrivacy/Dataset.lean create mode 100644 RandomDo/DifferentialPrivacy/Gaussian.lean create mode 100644 RandomDo/DifferentialPrivacy/Mean.lean create mode 100644 RandomDo/DifferentialPrivacy/Programs.lean create mode 100644 Test/DifferentialPrivacy.lean diff --git a/README.md b/README.md index 5ba5618..b9a5fba 100644 --- a/README.md +++ b/README.md @@ -1 +1,109 @@ -# Random-do notation \ No newline at end of file +# Random-do notation + +RandomDo writes probabilistic algorithms in `rdo`. The same program can be interpreted as a +mathematical measure for proofs or instantiated with an executable sampling backend. + +## Differential privacy + +Import `RandomDo` (or `RandomDo.DifferentialPrivacy`) and open `DifferentialPrivacy`. + +### The Gaussian `rdo` samplers + +The algorithms are in [`RandomDo/DifferentialPrivacy/Programs.lean`](RandomDo/DifferentialPrivacy/Programs.lean): + +- `gaussianProgram center σ` draws zero-mean Gaussian noise and returns `center + noise`. +- `gaussianCoordinates center σ` does this independently for each coordinate. +- `gaussianMeanRealProgram f D c n xs` computes the scalar empirical mean and adds noise. +- `gaussianMeanProgram f D c n xs` computes the vector empirical mean and adds independent noise + in each coordinate. + +The full scalar mean algorithm is: + +```lean +def gaussianMeanRealProgram {α : Type*} {R V : Type} [Scalar R] [Scalar V] + [HasGaussian m R V R] (f : α → R) (D c : V) (n : ℕ) (xs : Dataset α) : m R := rdo + let center := meanValue f xs + let σ := c * D / (n : V) + let z ← gaussianProgram (m := m) center σ + return z +``` + +Here `m` is an arbitrary `MeasurableSpaceMonad`. `meanValue` is pure arithmetic, and +`gaussianProgram` samples through `HasGaussian` in `rdo`. The vector version uses the same +computation coordinatewise. There is one implementation of each algorithm. + +`D` is a public upper bound on the domain's ℓ₂ diameter, `n > 0` is a public lower bound on +sample size, and `c` is a public noise multiplier. The standard deviation is `c * D / n`; +`HasGaussian` takes **variance**, so the sampler passes its square. + +At `m := Measure`, `R := ℝ`, and `V := ℝ≥0`, the programs denote exact real distributions. +The theorems `gaussianMeanRealProgram_eq_mechanism` and `gaussianMeanProgram_eq_mechanism` +identify these complete programs with the Gaussian laws used in the privacy proofs. +Choosing another interpretation runs these same definitions. The existing floating-point +backend is exercised in `Test.DifferentialPrivacy`; its arithmetic and generator are not part +of the exact-real privacy guarantee. + +### Privacy of the programs + +The following proves privacy of the actual vector `rdo` sampler under adding or removing one +record. `Mechanism.ofMeasure` only pairs the program with its proof of total probability one. + +```lean +import RandomDo + +open DifferentialPrivacy MeasureTheory +open scoped NNReal + +example {α : Type*} {d : ℕ} (f : α → EuclideanSpace ℝ (Fin d)) + {D ε δ : ℝ≥0} (hD : HasDiameter f D) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast 10 Dataset.AddRemove) ε δ + (Mechanism.ofMeasure + (gaussianMeanProgram (m := Measure) (fun a ↦ ⇑(f a)) D + (gaussianNoiseMultiplier ε δ) 10) (fun _ ↦ inferInstance)) := + gaussianMeanProgram_approxDP_addRemove hD (by norm_num) hε hδ hδ1 +``` + +`gaussianMeanProgram_approxDP_replaceOne` covers replacement. The corresponding scalar theorems +are prefixed `gaussianMeanRealProgram_approxDP`. Zero diameter is supported and requires no noise. + +For `ε > 0` and `0 < δ ≤ 1`, `gaussianNoiseMultiplier ε δ` supplies the multiplier: + +```text +t = sqrt(2 log(1/δ)) +c = (t + sqrt(t² + 2ε)) / (2ε) +σ = c * D / n +``` + +This sufficient calibration follows from a Gaussian Chernoff bound and works for every positive +`ε`. The proof establishes the joint density ratio, a dimension-independent directional tail +bound, and the DP event inequality. See +[Dwork and Roth, Appendix A](https://www.cis.upenn.edu/~aaroth/Papers/privacybook.pdf) for the +Gaussian privacy-loss argument; this calibration solves the Chernoff inequality directly. + +### Theory and assumptions + +- `Dataset α` is `List α`: finite sequences of arbitrary length, allowing repeated records. +- `Dataset.AddRemove` inserts or removes one record at any position; `Dataset.ReplaceOne` + replaces one record while preserving length. +- `Mechanism X Y` maps inputs to `ProbabilityMeasure Y`. +- `PureDP adj ε M` means `P(M x ∈ A) ≤ exp(ε) P(M x' ∈ A)` for adjacent inputs and + measurable output events. +- `ApproxDP adj ε δ M` adds `δ` to the right-hand side. Nonconstant Gaussian releases generally + require this approximate notion. + +The theory includes measurable deterministic postprocessing, restriction of adjacency, +adjacency-preserving input transformations, and monotonicity in privacy budgets. + +`HasDiameter f D` bounds all pairs of records in the public domain. For vectors, use an embedding +into `EuclideanSpace ℝ (Fin d)` to express the ℓ₂ norm. A bound on each coordinate alone is not an +ℓ₂ diameter bound. If both datasets have at least `n > 0` records, the empirical mean has +sensitivity at most `D / n` under either adjacency relation. Inserting into a nonempty dataset +has the sharper bound `D / (length + 1)`. + +The programs accept their parameters directly; the privacy theorems state the conditions on +those parameters and the inputs. `n` and `D` must be public. Choosing the variance from the +private dataset size or its observed diameter is not justified by these theorems. The real mean +of an empty list is defined as zero, but the mean privacy theorems require nonempty datasets. + +Run the library, proofs, and execution checks with `lake build RandomDo Test`. diff --git a/RandomDo.lean b/RandomDo.lean index b2d4043..4d6d433 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -1,5 +1,6 @@ module -- shake: keep-all --deprecated_module: ignore +public import RandomDo.DifferentialPrivacy public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding public import RandomDo.Measurable public import RandomDo.Monad.ForInInstances diff --git a/RandomDo/DifferentialPrivacy.lean b/RandomDo/DifferentialPrivacy.lean new file mode 100644 index 0000000..2c710fd --- /dev/null +++ b/RandomDo/DifferentialPrivacy.lean @@ -0,0 +1,13 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDo.DifferentialPrivacy.Basic +public import RandomDo.DifferentialPrivacy.Dataset +public import RandomDo.DifferentialPrivacy.Mean +public import RandomDo.DifferentialPrivacy.Gaussian +public import RandomDo.DifferentialPrivacy.Calibration +public import RandomDo.DifferentialPrivacy.Programs diff --git a/RandomDo/DifferentialPrivacy/Basic.lean b/RandomDo/DifferentialPrivacy/Basic.lean new file mode 100644 index 0000000..2ba880d --- /dev/null +++ b/RandomDo/DifferentialPrivacy/Basic.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure +public import Mathlib.Analysis.SpecialFunctions.Exp + +/-! +# Differential privacy + +A `Mechanism X Y` assigns a probability distribution on `Y` to each input in `X`. +There is no measurable-space requirement on inputs: privacy compares individual inputs. +`ApproxDP` quantifies over measurable output events and an explicit adjacency relation. +`PureDP` is its specialization to `δ = 0`. + +Privacy parameters are nonnegative reals. Allowing `δ ≥ 1` is convenient for bounds, although +only `δ < 1` is informative. No finite-precision sampler is identified with an exact real law. +-/ + +@[expose] public section + +open MeasureTheory +open scoped ENNReal NNReal + +namespace DifferentialPrivacy + +universe u v w + +/-- A probabilistic algorithm, specified by its output law at each input. -/ +abbrev Mechanism (X : Type u) (Y : Type v) [MeasurableSpace Y] := X → ProbabilityMeasure Y + +namespace Mechanism + +variable {X : Type u} {Y : Type v} {Z : Type w} + [MeasurableSpace Y] [MeasurableSpace Z] + +/-- Package a measure-valued algorithm with proofs that all its laws have mass one. -/ +def ofMeasure (M : X → Measure Y) (hM : ∀ x, IsProbabilityMeasure (M x)) : Mechanism X Y := + fun x ↦ ⟨M x, hM x⟩ + +/-- Measurable deterministic postprocessing of a mechanism. -/ +noncomputable def postprocess (M : Mechanism X Y) (f : Y → Z) (hf : Measurable f) : + Mechanism X Z := fun x ↦ (M x).map hf.aemeasurable + +end Mechanism + +variable {X : Type u} {Y : Type v} {Z : Type w} + [MeasurableSpace Y] [MeasurableSpace Z] + +/-- The directed event inequality underlying approximate differential privacy. Symmetry is +supplied by a symmetric adjacency relation when using `ApproxDP`. -/ +def DistributionLE (ε δ : ℝ≥0) (μ ν : Measure Y) : Prop := + ∀ A, MeasurableSet A → μ A ≤ ENNReal.ofReal (Real.exp ε) * ν A + δ + +/-- `(ε, δ)` differential privacy relative to `adj`. -/ +def ApproxDP (adj : X → X → Prop) (ε δ : ℝ≥0) (M : Mechanism X Y) : Prop := + ∀ ⦃x x'⦄, adj x x' → DistributionLE ε δ (M x : Measure Y) (M x' : Measure Y) + +/-- Pure `ε` differential privacy: `P(M x ∈ A) ≤ exp ε * P(M x' ∈ A)`. -/ +def PureDP (adj : X → X → Prop) (ε : ℝ≥0) (M : Mechanism X Y) : Prop := + ApproxDP adj ε 0 M + +namespace DistributionLE + +variable {ε ε' δ δ' : ℝ≥0} {μ ν : Measure Y} + +theorem refl (μ : Measure Y) : DistributionLE 0 0 μ μ := by + intro A _ + simp + +/-- A larger privacy budget preserves the event inequality. -/ +theorem mono (h : DistributionLE ε δ μ ν) (hε : ε ≤ ε') (hδ : δ ≤ δ') : + DistributionLE ε' δ' μ ν := by + intro A hA + exact (h A hA).trans (add_le_add + (mul_le_mul' (ENNReal.ofReal_le_ofReal (Real.exp_le_exp.mpr hε)) le_rfl) + (ENNReal.coe_le_coe.mpr hδ)) + +theorem map (h : DistributionLE ε δ μ ν) {f : Y → Z} (hf : Measurable f) : + DistributionLE ε δ (μ.map f) (ν.map f) := by + intro A hA + simpa only [Measure.map_apply hf hA] using h (f ⁻¹' A) (hf hA) + +/-- It suffices to dominate the measure on a good event and bound its complement. -/ +theorem of_goodSet {G : Set Y} (hG : MeasurableSet G) + (hgood : ∀ A, MeasurableSet A → μ (A ∩ G) ≤ ENNReal.ofReal (Real.exp ε) * ν A) + (hbad : μ Gᶜ ≤ δ) : DistributionLE ε δ μ ν := by + intro A hA + calc + μ A = μ (A ∩ G) + μ (A \ G) := (measure_inter_add_sdiff A hG).symm + _ ≤ ENNReal.ofReal (Real.exp ε) * ν A + δ := + add_le_add (hgood A hA) ((measure_mono (Set.sdiff_subset_compl A G)).trans hbad) + +end DistributionLE + +namespace ApproxDP + +variable {adj adj' : X → X → Prop} {ε ε' δ δ' : ℝ≥0} {M : Mechanism X Y} + +theorem mono (h : ApproxDP adj ε δ M) (hε : ε ≤ ε') (hδ : δ ≤ δ') : + ApproxDP adj ε' δ' M := fun _ _ hxx' ↦ (h hxx').mono hε hδ + +/-- Privacy for a relation also holds for any subrelation. -/ +theorem of_subrelation (h : ApproxDP adj ε δ M) (hadj : ∀ x x', adj' x x' → adj x x') : + ApproxDP adj' ε δ M := fun _ _ hxx' ↦ h (hadj _ _ hxx') + +theorem postprocess (h : ApproxDP adj ε δ M) {f : Y → Z} (hf : Measurable f) : + ApproxDP adj ε δ (M.postprocess f hf) := fun _ _ hxx' ↦ (h hxx').map hf + +/-- Preprocessing is allowed when it preserves adjacency. In particular this restricts a +mechanism to a public input domain, such as datasets of size at least `n`. -/ +theorem precompose {W : Type*} {rel : W → W → Prop} (h : ApproxDP adj ε δ M) + (f : W → X) (hf : ∀ x x', rel x x' → adj (f x) (f x')) : + ApproxDP rel ε δ (M ∘ f) := fun _ _ hxx' ↦ h (hf _ _ hxx') + +theorem const (adj : X → X → Prop) (μ : ProbabilityMeasure Y) : + ApproxDP adj 0 0 (fun _ : X ↦ μ) := fun _ _ _ ↦ DistributionLE.refl (μ : Measure Y) + +end ApproxDP + +theorem pureDP_iff {adj : X → X → Prop} {ε : ℝ≥0} {M : Mechanism X Y} : + PureDP adj ε M ↔ ∀ ⦃x x'⦄, adj x x' → ∀ A, MeasurableSet A → + (M x : Measure Y) A ≤ ENNReal.ofReal (Real.exp ε) * (M x' : Measure Y) A := by + simp [PureDP, ApproxDP, DistributionLE] + +end DifferentialPrivacy diff --git a/RandomDo/DifferentialPrivacy/Calibration.lean b/RandomDo/DifferentialPrivacy/Calibration.lean new file mode 100644 index 0000000..c6ffdda --- /dev/null +++ b/RandomDo/DifferentialPrivacy/Calibration.lean @@ -0,0 +1,167 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDo.DifferentialPrivacy.Gaussian +import Mathlib.Tactic + +/-! +# Calibrating Gaussian noise + +For `ε > 0` and `0 < δ ≤ 1`, put `t = sqrt (2 log (1/δ))` and +`c = (t + sqrt (t² + 2ε)) / (2ε)`. Standard deviation `c * Δ` suffices for a query of +ℓ₂ sensitivity `Δ`. This solves the Gaussian Chernoff-bound inequality exactly, works for all +positive `ε`, and does not require the `ε < 1` restriction of the classical `1.25/δ` formula. +It is a sufficient calibration, not the optimal analytic Gaussian calibration. +-/ + +@[expose] public section + +open MeasureTheory +open scoped NNReal + +namespace DifferentialPrivacy + +/-- Gaussian tail parameter `sqrt (2 log (1/δ))`, written without a reciprocal inside the log. -/ +noncomputable def gaussianTail (δ : ℝ≥0) : ℝ≥0 := + .mk (Real.sqrt (-2 * Real.log δ)) (Real.sqrt_nonneg _) + +/-- Noise multiplier for a Gaussian mechanism. Valid privacy calibration requires `ε > 0` +and `0 < δ ≤ 1`; the function is total to simplify use in definitions. -/ +noncomputable def gaussianNoiseMultiplier (ε δ : ℝ≥0) : ℝ≥0 := + (gaussianTail δ + NNReal.sqrt ((gaussianTail δ) ^ 2 + 2 * ε)) / (2 * ε) + +theorem gaussianTail_exp {δ : ℝ≥0} (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + Real.exp (-(gaussianTail δ : ℝ) ^ 2 / 2) = δ := by + have hlog : Real.log (δ : ℝ) ≤ 0 := Real.log_nonpos (by positivity) hδ1 + have hs : 0 ≤ -2 * Real.log (δ : ℝ) := by linarith + simp only [gaussianTail, NNReal.coe_mk, Real.sq_sqrt hs] + convert Real.exp_log (show 0 < (δ : ℝ) from hδ) using 1 + congr 1 + ring + +theorem gaussianNoiseMultiplier_pos {ε : ℝ≥0} (hε : 0 < ε) (δ : ℝ≥0) : + 0 < gaussianNoiseMultiplier ε δ := by + unfold gaussianNoiseMultiplier + have hs : 0 < (gaussianTail δ) ^ 2 + 2 * ε := by positivity + exact div_pos (add_pos_of_nonneg_of_pos (by positivity) (NNReal.sqrt_pos.mpr hs)) + (by positivity) + +/-- The calibrated multiplier makes the Gaussian privacy-loss bound exactly `ε`. -/ +theorem gaussianNoiseMultiplier_budget {ε : ℝ≥0} (hε : 0 < ε) (δ : ℝ≥0) : + 1 / (2 * (gaussianNoiseMultiplier ε δ : ℝ) ^ 2) + + 1 / (gaussianNoiseMultiplier ε δ : ℝ) * gaussianTail δ = ε := by + let t : ℝ := gaussianTail δ + let s : ℝ := Real.sqrt (t ^ 2 + 2 * ε) + have ht : 0 ≤ t := (gaussianTail δ).coe_nonneg + have he : 0 < (ε : ℝ) := hε + have hs : 0 < s := Real.sqrt_pos.mpr (by positivity) + have hs2 : s ^ 2 = t ^ 2 + 2 * ε := Real.sq_sqrt (by positivity) + have hc : 0 < (gaussianNoiseMultiplier ε δ : ℝ) := gaussianNoiseMultiplier_pos hε δ + have hinv : (gaussianNoiseMultiplier ε δ : ℝ)⁻¹ = s - t := by + simp only [gaussianNoiseMultiplier, NNReal.coe_div, NNReal.coe_add, Real.coe_sqrt, + NNReal.coe_pow, NNReal.coe_mul, NNReal.coe_ofNat] + change (((t + s) / (2 * (ε : ℝ)))⁻¹) = s - t + rw [inv_div] + apply (div_eq_iff (by positivity : t + s ≠ 0)).mpr + nlinarith + calc + _ = ((gaussianNoiseMultiplier ε δ : ℝ)⁻¹) ^ 2 / 2 + + (gaussianNoiseMultiplier ε δ : ℝ)⁻¹ * t := by + dsimp [t] + field_simp + _ = (s - t) ^ 2 / 2 + (s - t) * t := by rw [hinv] + _ = ε := by nlinarith + +/-- A convenient standard deviation for a query of sensitivity `Δ`. -/ +noncomputable def gaussianStddev (Δ ε δ : ℝ≥0) : ℝ≥0 := gaussianNoiseMultiplier ε δ * Δ + +private theorem scaled_budget {Δ ε δ : ℝ≥0} (hΔ : 0 < Δ) (hε : 0 < ε) : + (Δ : ℝ) ^ 2 / (2 * (gaussianStddev Δ ε δ : ℝ) ^ 2) + + (Δ : ℝ) / (gaussianStddev Δ ε δ : ℝ) * gaussianTail δ ≤ ε := by + have hc : 0 < (gaussianNoiseMultiplier ε δ : ℝ) := gaussianNoiseMultiplier_pos hε δ + have hd : 0 < (Δ : ℝ) := hΔ + rw [← gaussianNoiseMultiplier_budget hε δ] + apply le_of_eq + simp only [gaussianStddev, NNReal.coe_mul] + field_simp + +variable {X ι : Type*} [Fintype ι] + +/-- A Gaussian mechanism calibrated directly from `(ε, δ)` is differentially private. -/ +theorem calibratedGaussian_approxDP {adj : X → X → Prop} {f : X → EuclideanSpace ℝ ι} + {Δ ε δ : ℝ≥0} (hf : HasSensitivity adj f Δ) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP adj ε δ (gaussianMechanism f (gaussianStddev Δ ε δ)) := by + by_cases hΔ : Δ = 0 + · subst Δ + exact gaussianMechanism_of_zero_sensitivity hf _ _ _ + · have hΔ' : 0 < Δ := bot_lt_iff_ne_bot.mpr hΔ + exact gaussianMechanism_approxDP hf + (mul_pos (gaussianNoiseMultiplier_pos hε δ) hΔ') + (scaled_budget hΔ' hε) (gaussianTail_exp hδ hδ1).le + +theorem calibratedGaussianReal_approxDP {adj : X → X → Prop} {f : X → ℝ} + {Δ ε δ : ℝ≥0} (hf : HasSensitivity adj f Δ) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP adj ε δ (gaussianMechanismReal f (gaussianStddev Δ ε δ)) := by + by_cases hΔ : Δ = 0 + · subst Δ + exact gaussianMechanismReal_of_zero_sensitivity hf _ _ _ + · have hΔ' : 0 < Δ := bot_lt_iff_ne_bot.mpr hΔ + exact gaussianMechanismReal_approxDP hf + (mul_pos (gaussianNoiseMultiplier_pos hε δ) hΔ') + (scaled_budget hΔ' hε) (gaussianTail_exp hδ hδ1).le + +variable {α : Type*} + +/-- A calibrated noisy mean satisfies approximate DP for any adjacency with the proved mean +sensitivity bound. Both insertion/removal and replacement corollaries follow below. -/ +theorem gaussianMean_calibrated {adj : Dataset α → Dataset α → Prop} + {f : α → EuclideanSpace ℝ ι} {D ε δ : ℝ≥0} {n : ℕ} + (hf : HasSensitivity adj (empiricalMean f) ((D : ℝ) / n)) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP adj ε δ (gaussianMean f D (gaussianNoiseMultiplier ε δ) n) := by + simpa only [gaussianMean, gaussianStddev, mul_div_assoc] using + calibratedGaussian_approxDP (Δ := D / n) hf hε hδ hδ1 + +theorem gaussianMeanReal_calibrated {adj : Dataset α → Dataset α → Prop} + {f : α → ℝ} {D ε δ : ℝ≥0} {n : ℕ} + (hf : HasSensitivity adj (empiricalMean f) ((D : ℝ) / n)) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP adj ε δ (gaussianMeanReal f D (gaussianNoiseMultiplier ε δ) n) := by + simpa only [gaussianMeanReal, gaussianStddev, mul_div_assoc] using + calibratedGaussianReal_approxDP (Δ := D / n) hf hε hδ hδ1 + +theorem gaussianMean_calibrated_addRemove {f : α → EuclideanSpace ℝ ι} {D ε δ : ℝ≥0} + {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.AddRemove) ε δ + (gaussianMean f D (gaussianNoiseMultiplier ε δ) n) := + gaussianMean_calibrated (sensitivity_empiricalMean_addRemove hD hn) hε hδ hδ1 + +theorem gaussianMean_calibrated_replaceOne {f : α → EuclideanSpace ℝ ι} {D ε δ : ℝ≥0} + {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.ReplaceOne) ε δ + (gaussianMean f D (gaussianNoiseMultiplier ε δ) n) := + gaussianMean_calibrated (sensitivity_empiricalMean_replaceOne hD hn) hε hδ hδ1 + +theorem gaussianMeanReal_calibrated_addRemove {f : α → ℝ} {D ε δ : ℝ≥0} + {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.AddRemove) ε δ + (gaussianMeanReal f D (gaussianNoiseMultiplier ε δ) n) := + gaussianMeanReal_calibrated (sensitivity_empiricalMean_addRemove hD hn) hε hδ hδ1 + +theorem gaussianMeanReal_calibrated_replaceOne {f : α → ℝ} {D ε δ : ℝ≥0} + {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.ReplaceOne) ε δ + (gaussianMeanReal f D (gaussianNoiseMultiplier ε δ) n) := + gaussianMeanReal_calibrated (sensitivity_empiricalMean_replaceOne hD hn) hε hδ hδ1 + +end DifferentialPrivacy diff --git a/RandomDo/DifferentialPrivacy/Dataset.lean b/RandomDo/DifferentialPrivacy/Dataset.lean new file mode 100644 index 0000000..443cfe1 --- /dev/null +++ b/RandomDo/DifferentialPrivacy/Dataset.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import Mathlib.Analysis.Normed.Module.Basic +public import Mathlib.Algebra.BigOperators.Group.List.Lemmas + +/-! +# Datasets, adjacency, and sensitivity + +Datasets are finite sequences of arbitrary length; order and repeated records are retained. +Insertion/removal may occur at any position. Replacement adjacency has a separate name, since +its sensitivity and sample-size assumptions differ from insertion/removal adjacency. +-/ + +@[expose] public section + +namespace DifferentialPrivacy + +universe u v + +/-- A finite sequence of records with no fixed bound on its size. -/ +abbrev Dataset (α : Type u) := List α + +namespace Dataset + +variable {α : Type u} + +/-- One record was inserted at an arbitrary position. -/ +def InsertOne (x y : Dataset α) : Prop := + ∃ l r a, x = l ++ r ∧ y = l ++ a :: r + +/-- Unbounded adjacency: insert or delete exactly one record. -/ +def AddRemove (x y : Dataset α) : Prop := InsertOne x y ∨ InsertOne y x + +/-- Bounded adjacency: replace one record at an arbitrary position. It is harmless to allow +the replacement record to equal the original record. -/ +def ReplaceOne (x y : Dataset α) : Prop := + ∃ l r a b, x = l ++ a :: r ∧ y = l ++ b :: r + +theorem AddRemove.symm {x y : Dataset α} (h : AddRemove x y) : AddRemove y x := Or.symm h + +theorem ReplaceOne.symm {x y : Dataset α} (h : ReplaceOne x y) : ReplaceOne y x := by + obtain ⟨l, r, a, b, rfl, rfl⟩ := h + exact ⟨l, r, b, a, rfl, rfl⟩ + +theorem InsertOne.length {x y : Dataset α} (h : InsertOne x y) : y.length = x.length + 1 := by + obtain ⟨l, r, a, rfl, rfl⟩ := h + simp [Nat.add_assoc] + +theorem AddRemove.length {x y : Dataset α} (h : AddRemove x y) : + y.length = x.length + 1 ∨ x.length = y.length + 1 := + h.elim (fun h ↦ Or.inl h.length) (fun h ↦ Or.inr h.length) + +theorem AddRemove.irrefl (x : Dataset α) : ¬ AddRemove x x := by + intro h + rcases h.length with h | h <;> omega + +theorem ReplaceOne.length {x y : Dataset α} (h : ReplaceOne x y) : x.length = y.length := by + obtain ⟨l, r, a, b, rfl, rfl⟩ := h + simp + +/-- Restrict an adjacency relation by a public lower bound on both dataset sizes. -/ +def AtLeast (n : ℕ) (adj : Dataset α → Dataset α → Prop) (x y : Dataset α) : Prop := + n ≤ x.length ∧ n ≤ y.length ∧ adj x y + +end Dataset + +variable {X : Type u} {E : Type v} [SeminormedAddCommGroup E] + +/-- A global sensitivity bound for a query. With `E = EuclideanSpace ℝ (Fin d)`, this uses +the Euclidean (ℓ₂) norm, not the sup norm on a function space. -/ +def HasSensitivity (adj : X → X → Prop) (f : X → E) (Δ : ℝ) : Prop := + ∀ ⦃x y⦄, adj x y → ‖f x - f y‖ ≤ Δ + +theorem HasSensitivity.mono {adj : X → X → Prop} {f : X → E} {Δ Δ' : ℝ} + (h : HasSensitivity adj f Δ) (hΔ : Δ ≤ Δ') : HasSensitivity adj f Δ' := + fun _ _ hxy ↦ (h hxy).trans hΔ + +/-- An upper bound on the diameter of an embedded record domain. -/ +def HasDiameter {α : Type*} (f : α → E) (D : ℝ) : Prop := ∀ a b, ‖f a - f b‖ ≤ D + +end DifferentialPrivacy diff --git a/RandomDo/DifferentialPrivacy/Gaussian.lean b/RandomDo/DifferentialPrivacy/Gaussian.lean new file mode 100644 index 0000000..9d72ba5 --- /dev/null +++ b/RandomDo/DifferentialPrivacy/Gaussian.lean @@ -0,0 +1,316 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDo.DifferentialPrivacy.Basic +public import RandomDo.DifferentialPrivacy.Mean +public import Mathlib.Probability.Distributions.Gaussian.Multivariate +public import Mathlib.Probability.Moments.SubGaussian +import Mathlib.MeasureTheory.Integral.Pi +import Mathlib.Tactic + +/-! +# The Gaussian mechanism + +Independent Gaussian noise with common standard deviation `σ` is added to each coordinate. +The output space is `EuclideanSpace`, so query sensitivity uses the ℓ₂ norm. +The variance passed to Mathlib is `σ ^ 2`. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory +open scoped NNReal ENNReal BigOperators + +namespace DifferentialPrivacy + +variable {ι X α : Type*} [Fintype ι] + +/-- The law of independent Gaussian coordinates with a common standard deviation. -/ +noncomputable def gaussianVector (μ : EuclideanSpace ℝ ι) (σ : ℝ≥0) : + ProbabilityMeasure (EuclideanSpace ℝ ι) := + ⟨(Measure.pi (fun i ↦ gaussianReal (μ i) (σ ^ 2))).map (WithLp.toLp 2), + Measure.isProbabilityMeasure_map (by fun_prop)⟩ + +/-- Release a vector-valued query with independent Gaussian noise in every coordinate. -/ +noncomputable def gaussianMechanism (f : X → EuclideanSpace ℝ ι) (σ : ℝ≥0) : + Mechanism X (EuclideanSpace ℝ ι) := fun x ↦ gaussianVector (f x) σ + +/-- Scalar Gaussian mechanism, with standard deviation rather than variance as its parameter. -/ +noncomputable def gaussianMechanismReal (f : X → ℝ) (σ : ℝ≥0) : Mechanism X ℝ := + Mechanism.ofMeasure (fun x ↦ gaussianReal (f x) (σ ^ 2)) (fun _ ↦ inferInstance) + +/-- Gaussian noise added to an empirical vector mean. `n` is a public positive lower bound on +dataset size and `D` is a public upper bound on the domain's ℓ₂ diameter. `noiseMultiplier` +controls the privacy budget; the standard deviation is `noiseMultiplier * D / n`. -/ +noncomputable def gaussianMean (f : α → EuclideanSpace ℝ ι) + (D noiseMultiplier : ℝ≥0) (n : ℕ) : Mechanism (Dataset α) (EuclideanSpace ℝ ι) := + gaussianMechanism (empiricalMean f) (noiseMultiplier * D / n) + +/-- Scalar specialization of the noisy mean. -/ +noncomputable def gaussianMeanReal (f : α → ℝ) (D noiseMultiplier : ℝ≥0) (n : ℕ) : + Mechanism (Dataset α) ℝ := + gaussianMechanismReal (empiricalMean f) (noiseMultiplier * D / n) + +@[simp] theorem gaussianMechanismReal_zero (f : X → ℝ) (x : X) : + (gaussianMechanismReal f 0 x : Measure ℝ) = Measure.dirac (f x) := by + simp [gaussianMechanismReal, Mechanism.ofMeasure] + +/-- The scalar mechanism is unbiased. -/ +theorem integral_gaussianMechanismReal (f : X → ℝ) (σ : ℝ≥0) (x : X) : + ∫ y, y ∂(gaussianMechanismReal f σ x : Measure ℝ) = f x := + integral_id_gaussianReal + +namespace Gaussian + +/-- Joint density of independent coordinates. -/ +noncomputable def density (μ : ι → ℝ) (v : ℝ≥0) (z : ι → ℝ) : ℝ≥0∞ := + ∏ i, gaussianPDF (μ i) v (z i) + +@[fun_prop] theorem measurable_density (μ : ι → ℝ) (v : ℝ≥0) : + Measurable (density μ v) := by unfold density; fun_prop + +theorem pi_eq_withDensity (μ : ι → ℝ) {v : ℝ≥0} (hv : v ≠ 0) : + Measure.pi (fun i ↦ gaussianReal (μ i) v) = + (Measure.pi (fun _ : ι ↦ (volume : Measure ℝ))).withDensity (density μ v) := by + classical + apply Measure.pi_eq + intro s hs + rw [withDensity_apply _ (MeasurableSet.univ_pi hs), Measure.restrict_pi_pi] + have hd : density μ v = fun z ↦ ENNReal.ofReal (∏ i, gaussianPDFReal (μ i) v (z i)) := by + funext z + rw [ENNReal.ofReal_prod_of_nonneg (fun i _ ↦ gaussianPDFReal_nonneg _ _ _)] + rfl + rw [hd, ← ofReal_integral_eq_lintegral_ofReal + (Integrable.fintype_prod (fun i ↦ (integrable_gaussianPDFReal (μ i) v).restrict)) + (ae_of_all _ (fun z ↦ Finset.prod_nonneg (fun i _ ↦ gaussianPDFReal_nonneg _ _ _))), + integral_fintype_prod_eq_prod, + ENNReal.ofReal_prod_of_nonneg (fun i _ ↦ integral_nonneg (gaussianPDFReal_nonneg _ _))] + exact Finset.prod_congr rfl (fun i _ ↦ (gaussianReal_apply_eq_integral (μ i) hv (s i)).symm) + +/-- Squared Euclidean distance of two vectors written as coordinate functions. -/ +noncomputable def sqDist (μ ν : ι → ℝ) : ℝ := ∑ i, (μ i - ν i) ^ 2 + +/-- The centered linear part of Gaussian privacy loss, before division by the variance. -/ +noncomputable def linearNoise (μ ν z : ι → ℝ) : ℝ := ∑ i, (μ i - ν i) * (z i - μ i) + +@[fun_prop] theorem measurable_linearNoise (μ ν : ι → ℝ) : Measurable (linearNoise μ ν) := by + unfold linearNoise + fun_prop + +theorem sqDist_nonneg (μ ν : ι → ℝ) : 0 ≤ sqDist μ ν := + Finset.sum_nonneg (fun _ _ ↦ sq_nonneg _) + +theorem sqDist_eq_norm (μ ν : EuclideanSpace ℝ ι) : sqDist μ ν = ‖μ - ν‖ ^ 2 := by + simp [sqDist, EuclideanSpace.real_norm_sq_eq] + +theorem sqDist_eq_zero_iff (μ ν : ι → ℝ) : sqDist μ ν = 0 ↔ μ = ν := by + classical + simp [sqDist, Finset.sum_eq_zero_iff_of_nonneg (fun i _ ↦ sq_nonneg (μ i - ν i)), + sub_eq_zero, funext_iff] + +private theorem pdf_ratio (μ ν z : ℝ) (v : ℝ≥0) : + gaussianPDF μ v z = ENNReal.ofReal + (Real.exp (((μ - ν) * (z - μ) + (μ - ν) ^ 2 / 2) / v)) * gaussianPDF ν v z := by + rw [gaussianPDF, gaussianPDF, ← ENNReal.ofReal_mul (Real.exp_pos _).le] + congr 1 + simp only [gaussianPDFReal] + rw [mul_left_comm, ← Real.exp_add] + congr 2 + ring + +/-- Exact likelihood-ratio identity for Gaussians of equal variance. -/ +theorem density_ratio (μ ν z : ι → ℝ) (v : ℝ≥0) : + density μ v z = ENNReal.ofReal + (Real.exp ((linearNoise μ ν z + sqDist μ ν / 2) / v)) * density ν v z := by + classical + unfold density + calc + _ = ∏ i, ENNReal.ofReal + (Real.exp (((μ i - ν i) * (z i - μ i) + (μ i - ν i) ^ 2 / 2) / v)) * + gaussianPDF (ν i) v (z i) := + Finset.prod_congr rfl (fun i _ ↦ pdf_ratio (μ i) (ν i) (z i) v) + _ = _ := ?_ + rw [Finset.prod_mul_distrib] + congr 1 + rw [← ENNReal.ofReal_prod_of_nonneg (fun i _ ↦ (Real.exp_pos _).le), ← Real.exp_sum] + congr 2 + simp only [linearNoise, sqDist, add_div, Finset.sum_add_distrib, Finset.sum_div] + +/-- Centered real Gaussian variables are sub-Gaussian with their variance as parameter. -/ +theorem subgaussian_centered (μ : ℝ) (v : ℝ≥0) : + HasSubgaussianMGF (fun z ↦ z - μ) v (gaussianReal μ v) := by + have h : HasSubgaussianMGF id v (gaussianReal 0 v) := by + refine ⟨fun t ↦ integrable_exp_mul_gaussianReal t, fun t ↦ ?_⟩ + simp [mgf_id_gaussianReal] + have hm : (gaussianReal μ v).map (fun z ↦ z - μ) = gaussianReal 0 v := by + simp [gaussianReal_map_sub_const] + rw [← hm] at h + exact h.of_map (by fun_prop) + +/-- The centered privacy loss has sub-Gaussian parameter `v * ‖μ - ν‖₂²`. -/ +theorem subgaussian_linearNoise (μ ν : ι → ℝ) (v : ℝ≥0) : + HasSubgaussianMGF (linearNoise μ ν) (v * .mk (sqDist μ ν) (sqDist_nonneg μ ν)) + (Measure.pi (fun i ↦ gaussianReal (μ i) v)) := by + classical + have hi := iIndepFun_pi (μ := fun i ↦ gaussianReal (μ i) v) + (X := fun i z ↦ (μ i - ν i) * (z - μ i)) (fun _ ↦ by fun_prop) + have hc (i : ι) := (subgaussian_centered (μ i) v).const_mul (μ i - ν i) + have hc' (i : ι) : HasSubgaussianMGF (fun z : ι → ℝ ↦ (μ i - ν i) * (z i - μ i)) + (.mk ((μ i - ν i) ^ 2) (sq_nonneg _) * v) + (Measure.pi (fun i ↦ gaussianReal (μ i) v)) := by + have hmap := (measurePreserving_eval (fun i ↦ gaussianReal (μ i) v) i).map_eq + have hci := hc i + rw [← hmap] at hci + exact HasSubgaussianMGF.of_map (μ := Measure.pi (fun i ↦ gaussianReal (μ i) v)) + (Y := fun z : ι → ℝ ↦ z i) (measurable_pi_apply i).aemeasurable hci + have h := HasSubgaussianMGF.sum_of_iIndepFun hi (s := Finset.univ) (fun i _ ↦ hc' i) + convert h using 1 + · rfl + · apply NNReal.eq + simp [sqDist, Finset.mul_sum, mul_comm] + +/-- A dimension-independent Gaussian tail estimate in the direction between two query values. -/ +theorem linearNoise_tail (μ ν : ι → ℝ) {σ : ℝ≥0} (hσ : 0 < σ) (hne : μ ≠ ν) + (t : ℝ≥0) : + (Measure.pi (fun i ↦ gaussianReal (μ i) (σ ^ 2))) + {z | (t : ℝ) * σ * Real.sqrt (sqDist μ ν) < linearNoise μ ν z} ≤ + ENNReal.ofReal (Real.exp (-(t : ℝ) ^ 2 / 2)) := by + have hs : 0 < sqDist μ ν := lt_of_le_of_ne (sqDist_nonneg μ ν) + (Ne.symm (fun h ↦ hne ((sqDist_eq_zero_iff μ ν).mp h))) + have hσ' : 0 < (σ : ℝ) := hσ + have ht : 0 ≤ (t : ℝ) * σ * Real.sqrt (sqDist μ ν) := by positivity + have h := (subgaussian_linearNoise μ ν (σ ^ 2)).measure_ge_le ht + simp only [NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_mk] at h + have heq : -((t : ℝ) * σ * Real.sqrt (sqDist μ ν)) ^ 2 / + (2 * ((σ : ℝ) ^ 2 * sqDist μ ν)) = -(t : ℝ) ^ 2 / 2 := by + simp only [mul_pow, Real.sq_sqrt hs.le] + field_simp + rw [heq] at h + calc + _ ≤ (Measure.pi (fun i ↦ gaussianReal (μ i) (σ ^ 2))) + {z | (t : ℝ) * σ * Real.sqrt (sqDist μ ν) ≤ linearNoise μ ν z} := + measure_mono (fun z (hz : (t : ℝ) * σ * Real.sqrt (sqDist μ ν) < linearNoise μ ν z) ↦ hz.le) + _ ≤ _ := (ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) (Real.exp_pos _).le).mpr h + +/-- Gaussian event inequality from sensitivity and a tail parameter. This is the quantitative +core of the Gaussian mechanism, including the case of equal query answers. -/ +theorem distributionLE_pi (μ ν : ι → ℝ) {σ Δ ε δ t : ℝ≥0} (hσ : 0 < σ) + (hΔ : Real.sqrt (sqDist μ ν) ≤ Δ) + (hbudget : (Δ : ℝ) ^ 2 / (2 * (σ : ℝ) ^ 2) + (Δ : ℝ) / σ * t ≤ ε) + (htail : Real.exp (-(t : ℝ) ^ 2 / 2) ≤ δ) : + DistributionLE ε δ (Measure.pi (fun i ↦ gaussianReal (μ i) (σ ^ 2))) + (Measure.pi (fun i ↦ gaussianReal (ν i) (σ ^ 2))) := by + classical + by_cases heq : μ = ν + · subst ν + exact (DistributionLE.refl _).mono (by positivity) (by positivity) + have hσ' : 0 < (σ : ℝ) := hσ + have hv : σ ^ 2 ≠ 0 := pow_ne_zero _ (ne_of_gt hσ) + have hs : sqDist μ ν ≤ (Δ : ℝ) ^ 2 := by + nlinarith [Real.sq_sqrt (sqDist_nonneg μ ν), Real.sqrt_nonneg (sqDist μ ν), + sq_nonneg ((Δ : ℝ) - Real.sqrt (sqDist μ ν))] + let G : Set (ι → ℝ) := {z | linearNoise μ ν z ≤ (t : ℝ) * σ * Real.sqrt (sqDist μ ν)} + have hG : MeasurableSet G := measurableSet_le (measurable_linearNoise μ ν) measurable_const + have hgood (z : ι → ℝ) (hz : z ∈ G) : + density μ (σ ^ 2) z ≤ ENNReal.ofReal (Real.exp ε) * density ν (σ ^ 2) z := by + change linearNoise μ ν z ≤ (t : ℝ) * σ * Real.sqrt (sqDist μ ν) at hz + rw [density_ratio μ ν z] + apply mul_le_mul' _ le_rfl + apply ENNReal.ofReal_le_ofReal + apply Real.exp_le_exp.mpr + change (linearNoise μ ν z + sqDist μ ν / 2) / (σ : ℝ) ^ 2 ≤ ε + calc + _ ≤ ((t : ℝ) * σ * Real.sqrt (sqDist μ ν) + sqDist μ ν / 2) / (σ : ℝ) ^ 2 := + div_le_div_of_nonneg_right (add_le_add hz le_rfl) (sq_nonneg _) + _ = sqDist μ ν / (2 * (σ : ℝ) ^ 2) + Real.sqrt (sqDist μ ν) / σ * t := by + field_simp + ring + _ ≤ (Δ : ℝ) ^ 2 / (2 * (σ : ℝ) ^ 2) + (Δ : ℝ) / σ * t := by gcongr + _ ≤ ε := hbudget + apply DistributionLE.of_goodSet hG + · intro A hA + rw [pi_eq_withDensity μ hv, pi_eq_withDensity ν hv, + withDensity_apply _ (hA.inter hG), withDensity_apply _ hA] + calc + _ ≤ ∫⁻ z in A ∩ G, ENNReal.ofReal (Real.exp ε) * density ν (σ ^ 2) z := + setLIntegral_mono (by fun_prop) (fun z hz ↦ hgood z hz.2) + _ ≤ ∫⁻ z in A, ENNReal.ofReal (Real.exp ε) * density ν (σ ^ 2) z := + lintegral_mono' (Measure.restrict_mono_set _ Set.inter_subset_left) le_rfl + _ = _ := lintegral_const_mul _ (measurable_density ν (σ ^ 2)) + · change (Measure.pi (fun i ↦ gaussianReal (μ i) (σ ^ 2))) + {z | ¬ linearNoise μ ν z ≤ (t : ℝ) * σ * Real.sqrt (sqDist μ ν)} ≤ δ + simp only [not_le] + exact (linearNoise_tail μ ν hσ heq t).trans (by + simpa only [ENNReal.ofReal_coe_nnreal] using ENNReal.ofReal_le_ofReal htail) + +end Gaussian + +/-- The Gaussian mechanism is `(ε, δ)`-DP whenever its sensitivity, standard deviation, and +tail parameter satisfy the displayed scalar inequalities. This bound is independent of the +number of output coordinates. -/ +theorem gaussianMechanism_approxDP {adj : X → X → Prop} {f : X → EuclideanSpace ℝ ι} + {σ Δ ε δ t : ℝ≥0} (hf : HasSensitivity adj f Δ) (hσ : 0 < σ) + (hbudget : (Δ : ℝ) ^ 2 / (2 * (σ : ℝ) ^ 2) + (Δ : ℝ) / σ * t ≤ ε) + (htail : Real.exp (-(t : ℝ) ^ 2 / 2) ≤ δ) : ApproxDP adj ε δ (gaussianMechanism f σ) := by + intro x y hxy + apply DistributionLE.map (f := WithLp.toLp 2) _ (by fun_prop) + apply Gaussian.distributionLE_pi (⇑(f x)) (⇑(f y)) hσ _ hbudget htail + simpa [Gaussian.sqDist_eq_norm, Real.sqrt_sq (norm_nonneg _)] using hf hxy + +/-- Scalar version of the Gaussian privacy theorem. -/ +theorem gaussianMechanismReal_approxDP {adj : X → X → Prop} {f : X → ℝ} + {σ Δ ε δ t : ℝ≥0} (hf : HasSensitivity adj f Δ) (hσ : 0 < σ) + (hbudget : (Δ : ℝ) ^ 2 / (2 * (σ : ℝ) ^ 2) + (Δ : ℝ) / σ * t ≤ ε) + (htail : Real.exp (-(t : ℝ) ^ 2 / 2) ≤ δ) : ApproxDP adj ε δ (gaussianMechanismReal f σ) := by + intro x y hxy + have h := Gaussian.distributionLE_pi (fun _ : Fin 1 ↦ f x) (fun _ : Fin 1 ↦ f y) + hσ (by simpa [Gaussian.sqDist, Real.sqrt_sq_eq_abs, Real.norm_eq_abs] using hf hxy) + hbudget htail + have hm := h.map (measurable_pi_apply (0 : Fin 1)) + change DistributionLE ε δ (gaussianReal (f x) (σ ^ 2)) (gaussianReal (f y) (σ ^ 2)) + simpa only [(measurePreserving_eval (fun _ : Fin 1 ↦ gaussianReal (f x) (σ ^ 2)) 0).map_eq, + (measurePreserving_eval (fun _ : Fin 1 ↦ gaussianReal (f y) (σ ^ 2)) 0).map_eq] using hm + +/-- A query of zero sensitivity needs no noise. -/ +theorem gaussianMechanism_of_zero_sensitivity {adj : X → X → Prop} + {f : X → EuclideanSpace ℝ ι} (hf : HasSensitivity adj f 0) (σ ε δ : ℝ≥0) : + ApproxDP adj ε δ (gaussianMechanism f σ) := by + intro x y hxy + have h : f x = f y := sub_eq_zero.mp (norm_eq_zero.mp (le_antisymm (hf hxy) (norm_nonneg _))) + simp only [gaussianMechanism, h] + exact (DistributionLE.refl _).mono (by positivity) (by positivity) + +theorem gaussianMechanismReal_of_zero_sensitivity {adj : X → X → Prop} + {f : X → ℝ} (hf : HasSensitivity adj f 0) (σ ε δ : ℝ≥0) : + ApproxDP adj ε δ (gaussianMechanismReal f σ) := by + intro x y hxy + have h : f x = f y := sub_eq_zero.mp (norm_eq_zero.mp (le_antisymm (hf hxy) (norm_nonneg _))) + simp only [gaussianMechanismReal, Mechanism.ofMeasure, h] + exact (DistributionLE.refl _).mono (by positivity) (by positivity) + +/-- Privacy of the noisy mean under insertion/removal adjacency and a public minimum size. -/ +theorem gaussianMean_approxDP {f : α → EuclideanSpace ℝ ι} {D noiseMultiplier ε δ t : ℝ≥0} + {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) (hσ : 0 < noiseMultiplier * D / n) + (hbudget : ((D : ℝ) / n) ^ 2 / (2 * ((noiseMultiplier : ℝ) * D / n) ^ 2) + + ((D : ℝ) / n) / ((noiseMultiplier : ℝ) * D / n) * t ≤ ε) + (htail : Real.exp (-(t : ℝ) ^ 2 / 2) ≤ δ) : + ApproxDP (Dataset.AtLeast n Dataset.AddRemove) ε δ (gaussianMean f D noiseMultiplier n) := + gaussianMechanism_approxDP (Δ := D / n) + (sensitivity_empiricalMean_addRemove hD hn) hσ hbudget htail + +/-- The same fixed noise scale protects replacement adjacency. -/ +theorem gaussianMean_replaceOne_approxDP {f : α → EuclideanSpace ℝ ι} + {D noiseMultiplier ε δ t : ℝ≥0} {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) + (hσ : 0 < noiseMultiplier * D / n) + (hbudget : ((D : ℝ) / n) ^ 2 / (2 * ((noiseMultiplier : ℝ) * D / n) ^ 2) + + ((D : ℝ) / n) / ((noiseMultiplier : ℝ) * D / n) * t ≤ ε) + (htail : Real.exp (-(t : ℝ) ^ 2 / 2) ≤ δ) : + ApproxDP (Dataset.AtLeast n Dataset.ReplaceOne) ε δ (gaussianMean f D noiseMultiplier n) := + gaussianMechanism_approxDP (Δ := D / n) + (sensitivity_empiricalMean_replaceOne hD hn) hσ hbudget htail + +end DifferentialPrivacy diff --git a/RandomDo/DifferentialPrivacy/Mean.lean b/RandomDo/DifferentialPrivacy/Mean.lean new file mode 100644 index 0000000..5c88d06 --- /dev/null +++ b/RandomDo/DifferentialPrivacy/Mean.lean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDo.DifferentialPrivacy.Dataset +import Mathlib.Tactic + +/-! +# Sensitivity of the empirical mean + +The query is defined on lists of records mapped into a real normed space. Its sensitivity +theorems apply to nonempty datasets with a public lower bound on size. The value at the empty +dataset is zero by convention; a diameter bound alone does not control its distance to the +domain. In particular, the theorems deliberately do not cover empty/nonempty adjacency. +-/ + +@[expose] public section + +namespace DifferentialPrivacy + +variable {α E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +/-- Arithmetic mean of the embedded records, with value zero on the empty dataset. -/ +noncomputable def empiricalMean (f : α → E) (x : Dataset α) : E := + (x.length : ℝ)⁻¹ • (x.map f).sum + +@[simp] theorem empiricalMean_nil (f : α → E) : empiricalMean f [] = 0 := by + simp [empiricalMean] + +@[simp] theorem empiricalMean_singleton (f : α → E) (a : α) : + empiricalMean f [a] = f a := by + simp [empiricalMean] + +theorem empiricalMean_perm (f : α → E) {x y : Dataset α} (h : x.Perm y) : + empiricalMean f x = empiricalMean f y := by + rw [empiricalMean, empiricalMean, h.length_eq, (h.map f).sum_eq] + +private theorem sum_sub_const (f : α → E) (x : List α) (c : E) : + (x.map (fun a ↦ f a - c)).sum = (x.map f).sum - (x.length : ℝ) • c := by + induction x with + | nil => simp + | cons a x ih => + simp only [List.map_cons, List.sum_cons, List.length_cons, Nat.cast_add, Nat.cast_one, ih] + module + +omit [NormedSpace ℝ E] in +private theorem norm_sum_le_length (g : α → E) (x : List α) (D : ℝ) + (h : ∀ a ∈ x, ‖g a‖ ≤ D) : ‖(x.map g).sum‖ ≤ x.length * D := by + induction x with + | nil => simp + | cons a x ih => + simp only [List.map_cons, List.sum_cons, List.length_cons, Nat.cast_add, Nat.cast_one] + calc + ‖g a + (x.map g).sum‖ ≤ ‖g a‖ + ‖(x.map g).sum‖ := norm_add_le _ _ + _ ≤ D + x.length * D := add_le_add (h a (by simp)) (ih (by + intro b hb + exact h b (by simp [hb]))) + _ = (x.length + 1) * D := by ring + +/-- Every point of a bounded domain is within its diameter of the mean of a nonempty dataset. -/ +theorem norm_empiricalMean_sub_le {f : α → E} {D : ℝ} (hD : HasDiameter f D) + (x : Dataset α) (hx : x ≠ []) (a : α) : ‖empiricalMean f x - f a‖ ≤ D := by + have hn : (x.length : ℝ) ≠ 0 := by simpa using hx + have heq : empiricalMean f x - f a = + (x.length : ℝ)⁻¹ • (x.map (fun b ↦ f b - f a)).sum := by + rw [sum_sub_const, smul_sub, inv_smul_smul₀ hn] + rfl + rw [heq, norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr (Nat.cast_nonneg _))] + calc + (x.length : ℝ)⁻¹ * ‖(x.map (fun b ↦ f b - f a)).sum‖ ≤ + (x.length : ℝ)⁻¹ * (x.length * D) := + mul_le_mul_of_nonneg_left (norm_sum_le_length _ _ _ (fun b _ ↦ hD b a)) + (inv_nonneg.mpr (Nat.cast_nonneg _)) + _ = D := by field_simp + +/-- Inserting one record changes the mean by at most `D / (size + 1)`. -/ +theorem norm_empiricalMean_insert_le {f : α → E} {D : ℝ} (hD : HasDiameter f D) + {x y : Dataset α} (hxy : Dataset.InsertOne x y) (hx : x ≠ []) : + ‖empiricalMean f x - empiricalMean f y‖ ≤ D / y.length := by + obtain ⟨l, r, a, rfl, rfl⟩ := hxy + have hn : ((l ++ r).length : ℝ) ≠ 0 := by + simpa only [ne_eq, Nat.cast_eq_zero, List.length_eq_zero_iff] using hx + have hn1 : ((l ++ r).length : ℝ) + 1 ≠ 0 := by positivity + have hlen : (l ++ a :: r).length = (l ++ r).length + 1 := by simp [Nat.add_assoc] + have hsum : ((l ++ a :: r).map f).sum = ((l ++ r).map f).sum + f a := by + simp [add_comm, add_left_comm] + have heq : empiricalMean f (l ++ r) - empiricalMean f (l ++ a :: r) = + (((l ++ r).length : ℝ) + 1)⁻¹ • (empiricalMean f (l ++ r) - f a) := by + simp only [empiricalMean, hlen, Nat.cast_add, Nat.cast_one, hsum] + match_scalars <;> field_simp + ring + rw [heq, norm_smul, Real.norm_of_nonneg (by positivity)] + calc + _ ≤ (((l ++ r).length : ℝ) + 1)⁻¹ * D := + mul_le_mul_of_nonneg_left (norm_empiricalMean_sub_le hD _ hx a) (by positivity) + _ = D / (l ++ a :: r).length := by rw [hlen]; push_cast; ring + +/-- Replacing one record changes the mean by at most `D / size`. -/ +theorem norm_empiricalMean_replace_le {f : α → E} {D : ℝ} (hD : HasDiameter f D) + {x y : Dataset α} (hxy : Dataset.ReplaceOne x y) : + ‖empiricalMean f x - empiricalMean f y‖ ≤ D / x.length := by + obtain ⟨l, r, a, b, rfl, rfl⟩ := hxy + have heq : empiricalMean f (l ++ a :: r) - empiricalMean f (l ++ b :: r) = + ((l ++ a :: r).length : ℝ)⁻¹ • (f a - f b) := by + simp only [empiricalMean, List.length_append, List.length_cons, List.map_append, + List.map_cons, List.sum_append, List.sum_cons] + module + rw [heq, norm_smul, Real.norm_of_nonneg (by positivity)] + exact (mul_le_mul_of_nonneg_left (hD a b) (by positivity)).trans_eq (by rw [div_eq_mul_inv]; ring) + +/-- `D / n` is a global sensitivity bound for insertion/removal when both datasets have at +least the public, positive size `n`. The noise scale must use this public bound, not the actual +private length. -/ +theorem sensitivity_empiricalMean_addRemove {f : α → E} {D : ℝ} (hD : HasDiameter f D) + {n : ℕ} (hn : 0 < n) : + HasSensitivity (Dataset.AtLeast n Dataset.AddRemove) (empiricalMean f) (D / n) := by + intro x y ⟨hx, hy, hxy⟩ + have hx0 : x ≠ [] := by intro h; simp [h] at hx; omega + have hy0 : y ≠ [] := by intro h; simp [h] at hy; omega + have hD0 : 0 ≤ D := by + obtain ⟨a, ha⟩ := List.exists_mem_of_ne_nil x hx0 + simpa using hD a a + rcases hxy with hxy | hyx + · exact (norm_empiricalMean_insert_le hD hxy hx0).trans + (div_le_div_of_nonneg_left hD0 (by exact_mod_cast hn) (by exact_mod_cast hy)) + · rw [norm_sub_rev] + exact (norm_empiricalMean_insert_le hD hyx hy0).trans + (div_le_div_of_nonneg_left hD0 (by exact_mod_cast hn) (by exact_mod_cast hx)) + +/-- The same public `D / n` bound applies to replacement adjacency. -/ +theorem sensitivity_empiricalMean_replaceOne {f : α → E} {D : ℝ} (hD : HasDiameter f D) + {n : ℕ} (hn : 0 < n) : + HasSensitivity (Dataset.AtLeast n Dataset.ReplaceOne) (empiricalMean f) (D / n) := by + intro x y ⟨hx, _, hxy⟩ + have hD0 : 0 ≤ D := by + obtain ⟨l, r, a, b, _, _⟩ := hxy + simpa using hD a a + exact (norm_empiricalMean_replace_le hD hxy).trans + (div_le_div_of_nonneg_left hD0 (by exact_mod_cast hn) (by exact_mod_cast hx)) + +end DifferentialPrivacy diff --git a/RandomDo/DifferentialPrivacy/Programs.lean b/RandomDo/DifferentialPrivacy/Programs.lean new file mode 100644 index 0000000..a1a6c8d --- /dev/null +++ b/RandomDo/DifferentialPrivacy/Programs.lean @@ -0,0 +1,258 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDo.DifferentialPrivacy.Calibration +public import RandomDo.Tactic.Computable.Polymorphic.Polymorphic +public import RandomDo.Tactic.Computable.Polymorphic.Scalar +public import RandomDo.Monad.Notation +public import RandomDo.Measurable + +/-! +# Gaussian mechanisms as `rdo` programs + +`gaussianMeanRealProgram` and `gaussianMeanProgram` implement the whole noisy-mean algorithm: +compute the empirical mean, scale the noise by the public domain diameter and minimum size, +and add independent Gaussian noise. They use the same polymorphic distribution interface as +other RandomDo programs. There is no separate implementation for an execution backend. + +At `m := Measure`, the programs have the Gaussian laws proved below, and their privacy theorems +apply directly to these programs. Instantiate the same definitions with another interpretation +to run them. The privacy proofs concern the exact real interpretation. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory +open scoped NNReal + +namespace DifferentialPrivacy + +universe v + +variable {m : (α : Type) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] + {R V : Type} [MeasurableSpace R] [Zero R] [Add R] [Mul V] [HasGaussian m R V R] + +/-- Draw a query answer with Gaussian noise of standard deviation `σ`. +`HasGaussian` takes variance, so the standard deviation is squared here. -/ +def gaussianProgram (center : R) (σ : V) : m R := rdo + let noise ← HasGaussian.gaussian (m := m) (0 : R) (σ * σ) + return center + noise + +/-- Draw independent Gaussian coordinates in index order. The dimension is public. -/ +def gaussianCoordinates : {d : ℕ} → (Fin d → R) → V → m (Fin d → R) + | 0, _, _ => rdo return Fin.elim0 + | d + 1, center, σ => rdo + let z ← gaussianProgram (m := m) (center 0) σ + let zs ← gaussianCoordinates (fun i : Fin d ↦ center i.succ) σ + return Fin.cons z zs + +/-- Arithmetic mean using only operations available to polymorphic programs. No measurable +structure on records is needed, since the input dataset is fixed before sampling. -/ +def meanValue {α : Type*} {R : Type} [Scalar R] (f : α → R) (xs : Dataset α) : R := + xs.foldr (fun x total ↦ f x + total) 0 / (xs.length : R) + +/-- Add Gaussian noise to a scalar empirical mean. `D` is a public bound on the domain diameter, +`n` is a public positive lower bound on dataset size, and `c` is a public noise multiplier. +The noise standard deviation is `c * D / n`, independently of the private dataset size. -/ +def gaussianMeanRealProgram {α : Type*} {R V : Type} [Scalar R] [Scalar V] + [HasGaussian m R V R] (f : α → R) (D c : V) (n : ℕ) (xs : Dataset α) : m R := rdo + let center := meanValue f xs + let σ := c * D / (n : V) + let z ← gaussianProgram (m := m) center σ + return z + +/-- Add independent Gaussian noise to every coordinate of an empirical mean. `D` bounds the +domain's ℓ₂ diameter; `n` and `c` have the same meaning as in `gaussianMeanRealProgram`. +The dimension is public and the same noise scale is used in every coordinate. -/ +def gaussianMeanProgram {α : Type*} {R V : Type} [Scalar R] [Scalar V] + [HasGaussian m R V R] {d : ℕ} (f : α → Fin d → R) (D c : V) (n : ℕ) + (xs : Dataset α) : m (Fin d → R) := rdo + let center := fun i ↦ meanValue (fun x ↦ f x i) xs + let σ := c * D / (n : V) + let z ← gaussianCoordinates (m := m) center σ + return z + +theorem gaussianProgram_real (center : ℝ) (σ : ℝ≥0) : + gaussianProgram (m := Measure) center σ = gaussianReal center (σ ^ 2) := by + simp only [gaussianProgram, HasGaussian.gaussian, mBind_def, mPure_def] + rw [Measure.bind_dirac_eq_map _ (by fun_prop), gaussianReal_map_const_add] + simp [pow_two] + +/-- The exact interpretation of the scalar `rdo` program is the certified mechanism. -/ +theorem gaussianProgram_eq_mechanism {X : Type*} (f : X → ℝ) (σ : ℝ≥0) (x : X) : + gaussianProgram (m := Measure) (f x) σ = (gaussianMechanismReal f σ x : Measure ℝ) := by + simpa [gaussianMechanismReal, Mechanism.ofMeasure] using gaussianProgram_real (f x) σ + +/-- The exact interpretation of the recursive sampler has independent Gaussian coordinates. -/ +theorem gaussianCoordinates_real {d : ℕ} (center : Fin d → ℝ) (σ : ℝ≥0) : + gaussianCoordinates (m := Measure) center σ = + Measure.pi (fun i ↦ gaussianReal (center i) (σ ^ 2)) := by + induction d with + | zero => + exact (Measure.pi_of_empty (fun i ↦ gaussianReal (center i) (σ ^ 2)) Fin.elim0).symm + | succ d ih => + simp only [gaussianCoordinates, gaussianProgram_real, ih, + mBind_def, mPure_def] + have hcons (a : ℝ) : Measurable (Fin.cons (n := d) (α := fun _ ↦ ℝ) a) := by + apply measurable_pi_lambda + intro i + refine Fin.cases ?_ (fun j ↦ ?_) i + · simp + · simpa using (measurable_pi_apply j : Measurable (fun z : Fin d → ℝ ↦ z j)) + simp_rw [Measure.bind_dirac_eq_map _ (hcons _)] + have hp := (measurePreserving_piFinSuccAbove + (fun i ↦ gaussianReal (center i) (σ ^ 2)) (0 : Fin (d + 1))).symm.map_eq + simp only [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv, + Fin.insertNth_zero, Fin.zero_succAbove, Equiv.coe_fn_mk, cast_eq] at hp + rw [← hp] + ext A hA + have hm : Measurable (fun a : ℝ ↦ + (Measure.pi (fun i : Fin d ↦ gaussianReal (center i.succ) (σ ^ 2))).map + (Fin.cons (n := d) (α := fun _ ↦ ℝ) a)) := by + apply Measure.measurable_of_measurable_coe + intro B hB + simp only [Measure.map_apply (hcons _) hB] + exact measurable_measure_prodMk_left (measurable_finCons hB) + rw [Measure.bind_apply hA hm.aemeasurable, Measure.map_apply measurable_finCons hA, + Measure.prod_apply (measurable_finCons hA)] + apply lintegral_congr_ae + filter_upwards [] with a + exact Measure.map_apply (hcons a) hA + +/-- Mapping the coordinate program to Euclidean space gives the certified vector mechanism. -/ +theorem gaussianCoordinates_eq_mechanism {X : Type*} {d : ℕ} + (f : X → EuclideanSpace ℝ (Fin d)) (σ : ℝ≥0) (x : X) : + (gaussianCoordinates (m := Measure) (⇑(f x)) σ).map (WithLp.toLp 2) = + (gaussianMechanism f σ x : Measure (EuclideanSpace ℝ (Fin d))) := by + rw [gaussianCoordinates_real] + rfl + +/-- The pure arithmetic in the program computes the mathematical empirical mean. -/ +theorem meanValue_real {α : Type*} (f : α → ℝ) (xs : Dataset α) : + meanValue f xs = empiricalMean f xs := by + have hsum : xs.foldr (fun x total ↦ f x + total) 0 = (xs.map f).sum := by + induction xs with + | nil => rfl + | cons a xs ih => simp [ih] + simp only [meanValue, empiricalMean, hsum, smul_eq_mul, div_eq_mul_inv, mul_comm] + +/-- Taking a coordinate commutes with the empirical mean in Euclidean space. -/ +theorem empiricalMean_apply {α : Type*} {d : ℕ} (f : α → EuclideanSpace ℝ (Fin d)) + (xs : Dataset α) (i : Fin d) : + empiricalMean f xs i = empiricalMean (fun a ↦ f a i) xs := by + have hsum : (xs.map f).sum i = (xs.map (fun a ↦ f a i)).sum := by + induction xs with + | nil => rfl + | cons a xs ih => simpa using congrArg (f a i + ·) ih + simpa only [empiricalMean, PiLp.smul_apply, smul_eq_mul] using + congrArg ((xs.length : ℝ)⁻¹ * ·) hsum + +/-- The exact law of the complete scalar `rdo` mean algorithm. -/ +theorem gaussianMeanRealProgram_eq_mechanism {α : Type*} (f : α → ℝ) + (D c : ℝ≥0) (n : ℕ) (xs : Dataset α) : + gaussianMeanRealProgram (m := Measure) f D c n xs = + (gaussianMeanReal f D c n xs : Measure ℝ) := by + simp [gaussianMeanRealProgram, gaussianProgram_real, meanValue_real, + gaussianMeanReal, gaussianMechanismReal, Mechanism.ofMeasure] + +/-- The exact law of the complete vector `rdo` mean algorithm, in Euclidean coordinates. -/ +theorem gaussianMeanProgram_eq_mechanism {α : Type*} {d : ℕ} + (f : α → EuclideanSpace ℝ (Fin d)) (D c : ℝ≥0) (n : ℕ) (xs : Dataset α) : + (gaussianMeanProgram (m := Measure) (fun a ↦ ⇑(f a)) D c n xs).map (WithLp.toLp 2) = + (gaussianMean f D c n xs : Measure (EuclideanSpace ℝ (Fin d))) := by + simpa [gaussianMeanProgram, meanValue_real, ← empiricalMean_apply, gaussianMean] using + gaussianCoordinates_eq_mechanism (empiricalMean f) (c * D / n) xs + +/-- The scalar program always denotes a probability measure, including at zero noise. -/ +instance {α : Type*} (f : α → ℝ) (D c : ℝ≥0) (n : ℕ) (xs : Dataset α) : + IsProbabilityMeasure (gaussianMeanRealProgram (m := Measure) f D c n xs) := by + rw [gaussianMeanRealProgram_eq_mechanism] + infer_instance + +/-- The vector program always denotes a probability measure, including in dimension zero. -/ +instance {α : Type*} {d : ℕ} (f : α → Fin d → ℝ) (D c : ℝ≥0) (n : ℕ) (xs : Dataset α) : + IsProbabilityMeasure (gaussianMeanProgram (m := Measure) f D c n xs) := by + simpa [gaussianMeanProgram, gaussianCoordinates_real] using + (inferInstance : IsProbabilityMeasure + (Measure.pi (fun i ↦ gaussianReal (meanValue (fun a ↦ f a i) xs) ((c * D / n) ^ 2)))) + +/-- The vector program's output law is the certified Euclidean law in ordinary coordinates. -/ +theorem gaussianMeanProgram_eq_coordinateLaw {α : Type*} {d : ℕ} + (f : α → EuclideanSpace ℝ (Fin d)) (D c : ℝ≥0) (n : ℕ) (xs : Dataset α) : + gaussianMeanProgram (m := Measure) (fun a ↦ ⇑(f a)) D c n xs = + (gaussianMean f D c n xs : Measure (EuclideanSpace ℝ (Fin d))).map WithLp.ofLp := by + rw [← gaussianMeanProgram_eq_mechanism, Measure.map_map (by fun_prop) (by fun_prop)] + simp [Function.comp_def] + +/-- Privacy of the scalar `rdo` program, from any proved empirical-mean sensitivity bound. +`Mechanism.ofMeasure` only packages the program with its probability proof. -/ +theorem gaussianMeanRealProgram_approxDP {α : Type*} {adj : Dataset α → Dataset α → Prop} + {f : α → ℝ} {D ε δ : ℝ≥0} {n : ℕ} + (hf : HasSensitivity adj (empiricalMean f) ((D : ℝ) / n)) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP adj ε δ (Mechanism.ofMeasure + (gaussianMeanRealProgram (m := Measure) f D (gaussianNoiseMultiplier ε δ) n) + (fun _ ↦ inferInstance)) := by + intro xs ys hxy + change DistributionLE ε δ (gaussianMeanRealProgram (m := Measure) _ _ _ _ xs) + (gaussianMeanRealProgram (m := Measure) _ _ _ _ ys) + simp only [gaussianMeanRealProgram_eq_mechanism] + exact gaussianMeanReal_calibrated hf hε hδ hδ1 hxy + +/-- Privacy of the vector `rdo` program. Sensitivity is measured in Euclidean space, so the +guarantee uses ℓ₂ sensitivity and has no extra factor depending on dimension. -/ +theorem gaussianMeanProgram_approxDP {α : Type*} {d : ℕ} + {adj : Dataset α → Dataset α → Prop} {f : α → EuclideanSpace ℝ (Fin d)} + {D ε δ : ℝ≥0} {n : ℕ} + (hf : HasSensitivity adj (empiricalMean f) ((D : ℝ) / n)) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP adj ε δ (Mechanism.ofMeasure + (gaussianMeanProgram (m := Measure) (fun a ↦ ⇑(f a)) D (gaussianNoiseMultiplier ε δ) n) + (fun _ ↦ inferInstance)) := by + intro xs ys hxy + change DistributionLE ε δ (gaussianMeanProgram (m := Measure) _ _ _ _ xs) + (gaussianMeanProgram (m := Measure) _ _ _ _ ys) + rw [gaussianMeanProgram_eq_coordinateLaw, gaussianMeanProgram_eq_coordinateLaw] + exact (gaussianMean_calibrated hf hε hδ hδ1 hxy).map (by fun_prop) + +/-- The scalar `rdo` mean program is private under insertion/removal of one record. -/ +theorem gaussianMeanRealProgram_approxDP_addRemove {α : Type*} {f : α → ℝ} + {D ε δ : ℝ≥0} {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.AddRemove) ε δ (Mechanism.ofMeasure + (gaussianMeanRealProgram (m := Measure) f D (gaussianNoiseMultiplier ε δ) n) + (fun _ ↦ inferInstance)) := + gaussianMeanRealProgram_approxDP (sensitivity_empiricalMean_addRemove hD hn) hε hδ hδ1 + +/-- The scalar `rdo` mean program is private under replacement of one record. -/ +theorem gaussianMeanRealProgram_approxDP_replaceOne {α : Type*} {f : α → ℝ} + {D ε δ : ℝ≥0} {n : ℕ} (hD : HasDiameter f D) (hn : 0 < n) + (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.ReplaceOne) ε δ (Mechanism.ofMeasure + (gaussianMeanRealProgram (m := Measure) f D (gaussianNoiseMultiplier ε δ) n) + (fun _ ↦ inferInstance)) := + gaussianMeanRealProgram_approxDP (sensitivity_empiricalMean_replaceOne hD hn) hε hδ hδ1 + +/-- The vector `rdo` mean program is private under insertion/removal of one record. -/ +theorem gaussianMeanProgram_approxDP_addRemove {α : Type*} {d : ℕ} + {f : α → EuclideanSpace ℝ (Fin d)} {D ε δ : ℝ≥0} {n : ℕ} + (hD : HasDiameter f D) (hn : 0 < n) (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.AddRemove) ε δ (Mechanism.ofMeasure + (gaussianMeanProgram (m := Measure) (fun a ↦ ⇑(f a)) D (gaussianNoiseMultiplier ε δ) n) + (fun _ ↦ inferInstance)) := + gaussianMeanProgram_approxDP (sensitivity_empiricalMean_addRemove hD hn) hε hδ hδ1 + +/-- The vector `rdo` mean program is private under replacement of one record. -/ +theorem gaussianMeanProgram_approxDP_replaceOne {α : Type*} {d : ℕ} + {f : α → EuclideanSpace ℝ (Fin d)} {D ε δ : ℝ≥0} {n : ℕ} + (hD : HasDiameter f D) (hn : 0 < n) (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast n Dataset.ReplaceOne) ε δ (Mechanism.ofMeasure + (gaussianMeanProgram (m := Measure) (fun a ↦ ⇑(f a)) D (gaussianNoiseMultiplier ε δ) n) + (fun _ ↦ inferInstance)) := + gaussianMeanProgram_approxDP (sensitivity_empiricalMean_replaceOne hD hn) hε hδ hδ1 + +end DifferentialPrivacy diff --git a/Test.lean b/Test.lean index bba557b..0e0bbc1 100644 --- a/Test.lean +++ b/Test.lean @@ -4,6 +4,7 @@ public import Test.Bind public import Test.Common public import Test.Computable public import Test.Control +public import Test.DifferentialPrivacy public import Test.Gaps public import Test.Instances public import Test.IsMarkov diff --git a/Test/DifferentialPrivacy.lean b/Test/DifferentialPrivacy.lean new file mode 100644 index 0000000..f799284 --- /dev/null +++ b/Test/DifferentialPrivacy.lean @@ -0,0 +1,150 @@ +module + +public import RandomDo +public meta import RandomDo.DifferentialPrivacy.Programs +import Mathlib.Tactic + +set_option linter.style.header false + +open DifferentialPrivacy MeasureTheory ProbabilityTheory +open scoped NNReal + +@[expose] public section + +namespace Test.DifferentialPrivacy + +-- Insertion works in the middle of a sequence and keeps multiplicities. +example : Dataset.AddRemove ([1, 2, 2] : Dataset ℕ) [1, 7, 2, 2] := + Or.inl ⟨[1], [2, 2], 7, rfl, rfl⟩ + +example : Dataset.AddRemove ([1, 7, 2, 2] : Dataset ℕ) [1, 2, 2] := + Dataset.AddRemove.symm (Or.inl ⟨[1], [2, 2], 7, rfl, rfl⟩) + +example : Dataset.AddRemove ([] : Dataset ℕ) [3] := Or.inl ⟨[], [], 3, rfl, rfl⟩ + +example : ¬ Dataset.AddRemove ([1, 2] : Dataset ℕ) [1, 3] := by + intro h + rcases h.length with h | h <;> norm_num at h + +example : Dataset.ReplaceOne ([1, 2] : Dataset ℕ) [1, 3] := + ⟨[1], [], 2, 3, rfl, rfl⟩ + +example : empiricalMean (id : ℝ → ℝ) [1, 2, 3] = 2 := by norm_num [empiricalMean] + +-- A diameter bound alone cannot protect the jump from an empty dataset to a translated domain. +example : ¬ HasSensitivity Dataset.AddRemove (empiricalMean (fun _ : Unit ↦ (100 : ℝ))) 0 := by + intro h + have h' := h (x := []) (y := [()]) (Or.inl ⟨[], [], (), rfl, rfl⟩) + norm_num at h' + +/-- A concrete bounded domain for the end-to-end privacy examples. -/ +theorem unitInterval_diameter : HasDiameter (fun x : Set.Icc (0 : ℝ) 1 ↦ (x : ℝ)) 1 := by + intro a b + rw [Real.norm_eq_abs, abs_le] + constructor <;> linarith [a.property.1, a.property.2, b.property.1, b.property.2] + +-- Privacy of the actual scalar rdo program, including epsilon > 1. +example : ApproxDP (Dataset.AtLeast 10 Dataset.AddRemove) 2 (1 / 100) + (Mechanism.ofMeasure + (gaussianMeanRealProgram (m := Measure) (fun x : Set.Icc (0 : ℝ) 1 ↦ (x : ℝ)) 1 + (gaussianNoiseMultiplier 2 (1 / 100)) 10) (fun _ ↦ inferInstance)) := + gaussianMeanRealProgram_approxDP_addRemove unitInterval_diameter (by norm_num) + (by norm_num) (by norm_num) (by norm_num [div_le_iff₀]) + +example {α : Type*} {d : ℕ} (f : α → EuclideanSpace ℝ (Fin d)) {D ε δ : ℝ≥0} + (hD : HasDiameter f D) (hε : 0 < ε) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : + ApproxDP (Dataset.AtLeast 10 Dataset.ReplaceOne) ε δ + (Mechanism.ofMeasure + (gaussianMeanProgram (m := Measure) (fun a ↦ ⇑(f a)) D + (gaussianNoiseMultiplier ε δ) 10) (fun _ ↦ inferInstance)) := + gaussianMeanProgram_approxDP_replaceOne hD (by norm_num) hε hδ hδ1 + +-- Zero diameter is supported by calibration, without requiring positive Gaussian variance. +example : ApproxDP (Dataset.AtLeast 1 Dataset.AddRemove) 1 (1 / 100) + (Mechanism.ofMeasure + (gaussianMeanRealProgram (m := Measure) (fun _ : Unit ↦ (100 : ℝ)) 0 + (gaussianNoiseMultiplier 1 (1 / 100)) 1) (fun _ ↦ inferInstance)) := by + apply gaussianMeanRealProgram_approxDP_addRemove + · intro a b; simp + all_goals norm_num [div_le_iff₀] + +example (ε δ : ℝ≥0) : gaussianStddev 0 ε δ = 0 := by simp [gaussianStddev] + +example (D ε δ : ℝ≥0) : gaussianStddev (2 * D) ε δ = 2 * gaussianStddev D ε δ := by + simp only [gaussianStddev] + ring + +example {X : Type*} (adj : X → X → Prop) (μ : ProbabilityMeasure ℝ) : + PureDP adj 0 (fun _ ↦ μ) := ApproxDP.const adj μ + +example {X : Type*} {adj : X → X → Prop} {ε δ : ℝ≥0} {M : Mechanism X ℝ} + (h : ApproxDP adj ε δ M) : ApproxDP adj ε δ (M.postprocess (fun x ↦ x + 1) (by fun_prop)) := + h.postprocess (by fun_prop) + +-- The recursive program is a product law, including zero output dimensions. +example {d : ℕ} (center : Fin d → ℝ) (σ : ℝ≥0) : + gaussianCoordinates (m := Measure) center σ = + Measure.pi (fun i ↦ gaussianReal (center i) (σ ^ 2)) := + gaussianCoordinates_real center σ + +-- The full program has the certified law, for arbitrary record embeddings and dataset lengths. +example {α : Type*} (f : α → ℝ) (D c : ℝ≥0) (n : ℕ) (xs : Dataset α) : + gaussianMeanRealProgram (m := Measure) f D c n xs = + (gaussianMeanReal f D c n xs : Measure ℝ) := + gaussianMeanRealProgram_eq_mechanism f D c n xs + +example {α : Type*} (f : α → ℝ) (c : ℝ≥0) (n : ℕ) (xs : Dataset α) : + gaussianMeanRealProgram (m := Measure) f 0 c n xs = Measure.dirac (empiricalMean f xs) := by + rw [gaussianMeanRealProgram_eq_mechanism] + simp [gaussianMeanReal] + +example : IsProbabilityMeasure + (gaussianMeanProgram (m := Measure) (id : (Fin 0 → ℝ) → Fin 0 → ℝ) + (0 : ℝ≥0) 1 1 [Fin.elim0]) := + inferInstance + +example : gaussianMeanRealProgram (m := Measure) (id : ℝ → ℝ) (2 : ℝ≥0) 3 2 [1, 3] = + gaussianReal 2 9 := by + rw [gaussianMeanRealProgram_eq_mechanism] + norm_num [gaussianMeanReal, gaussianMechanismReal, Mechanism.ofMeasure, empiricalMean] + +-- These commands only run the same rdo definitions with the project's existing sampling backend. +-- The algorithms themselves never depend on IO or on a particular random-number generator. +open NumLean + +run_cmd do + let actual ← IO.runRandPCGWith (m := IO) 42 + (gaussianMeanRealProgram (m := RandM) (id : Float → Float) (2 : Float) 3 2 [1, 3]) + let noise ← IO.runRandPCGWith (m := IO) 42 (NumLean.normal' 0 9) + unless actual == 2 + noise do throwError "incorrect scalar mean or Gaussian variance" + -- The actual private size changes the mean, but not the public noise scale. + let larger ← IO.runRandPCGWith (m := IO) 42 + (gaussianMeanRealProgram (m := RandM) (id : Float → Float) (2 : Float) 3 2 [1, 3, 1, 3]) + unless larger == actual do throwError "noise scale depends on private dataset size" + let doubled ← IO.runRandPCGWith (m := IO) 42 + (gaussianMeanRealProgram (m := RandM) (id : Float → Float) (4 : Float) 3 2 [1, 3]) + unless (doubled - (2 + 2 * noise)).abs < 1e-12 do + throwError "noise scale is not proportional to public diameter" + let halved ← IO.runRandPCGWith (m := IO) 42 + (gaussianMeanRealProgram (m := RandM) (id : Float → Float) (2 : Float) 3 4 [1, 3, 1, 3]) + unless (halved - (2 + noise / 2)).abs < 1e-12 do + throwError "noise scale is not inversely proportional to public minimum size" + let noNoise ← IO.runRandPCGWith (m := IO) 42 + (gaussianMeanRealProgram (m := RandM) (id : Float → Float) (0 : Float) 3 2 [7, 7]) + unless noNoise == 7 do throwError "zero diameter added noise" + +run_cmd do + let actual ← IO.runRandPCGWith (m := IO) 42 + (gaussianMeanProgram (m := RandM) (id : (Fin 2 → Float) → Fin 2 → Float) + (5 : Float) 2 2 [![0, 0], ![3, 4]]) + let expected ← IO.runRandPCGWith (m := IO) 42 do + let x ← NumLean.normal' 0 25 + let y ← NumLean.normal' 0 25 + pure (1.5 + x, 2 + y) + unless actual 0 == expected.1 && actual 1 == expected.2 do + throwError "vector mean must use independent Gaussian coordinates in index order" + let _ ← IO.runRandPCGWith (m := IO) 42 + (gaussianMeanProgram (m := RandM) (id : (Fin 0 → Float) → Fin 0 → Float) + (5 : Float) 2 2 [Fin.elim0, Fin.elim0]) + +end Test.DifferentialPrivacy From feaec92c02013d20e71e7b6580e1ebd14d87b96c Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Wed, 14 Oct 2026 21:45:16 +0200 Subject: [PATCH 2/2] Include DP modules in the generated import index --- RandomDo.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/RandomDo.lean b/RandomDo.lean index 4d6d433..08cb5f6 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -1,6 +1,12 @@ module -- shake: keep-all --deprecated_module: ignore public import RandomDo.DifferentialPrivacy +public import RandomDo.DifferentialPrivacy.Basic +public import RandomDo.DifferentialPrivacy.Calibration +public import RandomDo.DifferentialPrivacy.Dataset +public import RandomDo.DifferentialPrivacy.Gaussian +public import RandomDo.DifferentialPrivacy.Mean +public import RandomDo.DifferentialPrivacy.Programs public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding public import RandomDo.Measurable public import RandomDo.Monad.ForInInstances