@@ -1 +1,109 @@
-# Random-do notation
+# 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`.
@@ -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
 
@@ -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
@@ -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