Differential privacy (learning theory)

This file introduces a small, reusable vocabulary for differential privacy (DP) in TorchLean’s learning-theory layer.

We isolate the core event-wise definition of differential privacy and the closure properties that show up when DP is connected to learning theory, stability, and verification pipelines.

We keep the definition general by parameterizing over:

• an adjacency relation Adj : α → α → Prop (e.g. “datasets differ in one example”), and
• a randomized mechanism M : α → ProbabilityMeasure β.

Then $(\varepsilon,\delta)$-DP is the standard event-wise bound:

$$ \Pr[M(a)\in S]\leq e^\varepsilon\Pr[M(a')\in S]+\delta $$

for all adjacent $a\sim a'$ and measurable events $S$.

We phrase this in mathlib using ProbabilityMeasure and Measure:

• M a is a ProbabilityMeasure β, and
• (M a : Measure β) S is the probability (as an ENNReal) of the event S.

This makes the definition work uniformly for discrete and continuous outputs, while keeping the measurability side-conditions explicit.

We also include a couple of basic structural lemmas that are easy to reuse downstream (and that are often needed to compose DP facts through a larger construction):

• monotonicity in δ and in ε, and
• post-processing (measurable mapping of outputs preserves DP).

Typical instantiations

• α is a dataset type, Adj means “replace/remove one example”.
• β is some model or statistic released to the outside world.
• M is a randomized training procedure / query mechanism.

In this repository, the stability development (see NN.MLTheory.LearningTheory.Stability.Core) uses datasets Tensor Z [n], with a Fin n → Z view, for a fixed sample size n. For DP, one can define Adj in terms of replacing one coordinate.

References

• Dwork, McSherry, Nissim & Smith (2006), “Calibrating Noise to Sensitivity in Private Data Analysis”.
• Dwork & Roth (2014), “The Algorithmic Foundations of Differential Privacy” (monograph).
• Post-processing is a standard closure property of DP; see, e.g., Dwork–Roth (2014).

Mechanisms

@[reducible, inline]

abbrev NN.MLTheory.LearningTheory.Mechanism (α β : Type) [MeasurableSpace β] : Type

A randomized mechanism from inputs α to outputs β.

We use ProbabilityMeasure β so probability mass is total ($\mu(\mathrm{univ})=1$) and so that post-processing can be phrased using ProbabilityMeasure.map (pushforward along a measurable function).

Differential privacy

def NN.MLTheory.LearningTheory.DifferentialPrivacy {α β : Type} (Adj : α → α → Prop) [MeasurableSpace β] (M : Mechanism α β) (ε : ℝ) (δ : ENNReal) : Prop

$(\varepsilon,\delta)$-differential privacy with respect to an adjacency relation Adj.

This is the standard “event-wise” definition:

for all adjacent inputs $a\sim a'$ and all measurable events $S$,

$$ \Pr[M(a)\in S]\leq e^\varepsilon\Pr[M(a')\in S]+\delta. $$

We write probabilities as measures (M a : Measure β) S so the inequality lives in ENNReal. The predicate imposes no symmetry on Adj, no nonnegativity condition on ε, and no upper bound on δ; callers supply the adjacency and budget restrictions needed for their application.

A common special case: $\delta=0$ (“pure DP”).

@[reducible, inline]

abbrev NN.MLTheory.LearningTheory.PureDP {α β : Type} (Adj : α → α → Prop) [MeasurableSpace β] (M : Mechanism α β) (ε : ℝ) : Prop

theorem NN.MLTheory.LearningTheory.differentialPrivacy_mono_delta {α β : Type} {Adj : α → α → Prop} [MeasurableSpace β] {M : Mechanism α β} {ε : ℝ} {δ₁ δ₂ : ENNReal} (hδ : δ₁ ≤ δ₂) : DifferentialPrivacy Adj M ε δ₁ → DifferentialPrivacy Adj M ε δ₂

$\delta$-monotonicity: if a mechanism is $(\varepsilon,\delta_1)$-DP and $\delta_1\leq\delta_2$, then it is also $(\varepsilon,\delta_2)$-DP.

This small lemma is useful when you:

• prove DP with a “clean” bound, then
• want to reuse it under a slightly looser $\delta$ (e.g. after taking a sup, or adding a slack term).

theorem NN.MLTheory.LearningTheory.differentialPrivacy_mono_eps {α β : Type} {Adj : α → α → Prop} [MeasurableSpace β] {M : Mechanism α β} {ε₁ ε₂ : ℝ} {δ : ENNReal} (hε : ε₁ ≤ ε₂) : DifferentialPrivacy Adj M ε₁ δ → DifferentialPrivacy Adj M ε₂ δ

$\varepsilon$-monotonicity: privacy at a smaller $\varepsilon$ implies privacy at a larger one.

Together with differentialPrivacy_mono_delta this says the predicate is monotone in the whole budget $(\varepsilon,\delta)$. That is what lets a pipeline advertise one budget for a step that was actually proved private at a tighter one, which happens constantly once several mechanisms are composed and their budgets are rounded to a common value.

The mathematical content is only monotonicity of Real.exp together with monotonicity of multiplication on ENNReal; we record it as a lemma so callers do not repeat that rewriting inline.

Post-processing

noncomputable def NN.MLTheory.LearningTheory.postprocess {α β γ : Type} [MeasurableSpace β] [MeasurableSpace γ] (M : Mechanism α β) (f : β → γ) (hf : Measurable f) : Mechanism α γ

Post-process a mechanism by applying a measurable function to its output.

In DP folklore: if M is DP, then so is f ∘ M for any (measurable) f that does not look at the private input. This is called post-processing and is one of the core reasons DP composes well with downstream pipelines.

Formally, postprocess M f is the pushforward measure (M a).map f for each input a.

theorem NN.MLTheory.LearningTheory.differentialPrivacy_postprocess {α β γ : Type} {Adj : α → α → Prop} [MeasurableSpace β] [MeasurableSpace γ] {M : Mechanism α β} {ε : ℝ} {δ : ENNReal} {f : β → γ} (hf : Measurable f) : DifferentialPrivacy Adj M ε δ → DifferentialPrivacy Adj (postprocess M f hf) ε δ

Post-processing theorem: measurable mappings of outputs preserve DP.

Proof idea (the standard one):

• the probability of an event S under the mapped output is the probability of the preimage f ⁻¹' S under the original output;
• apply DP for M to the measurable set f ⁻¹' S.