diff --git a/.gitignore b/.gitignore index 30dd9f7f..dabad31e 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ -.lake/** \ No newline at end of file +.lake/** + +.DS_Store \ No newline at end of file diff --git a/SampCert.lean b/SampCert.lean index 5a7ac53e..5e58156b 100644 --- a/SampCert.lean +++ b/SampCert.lean @@ -5,6 +5,7 @@ Authors: Jean-Baptiste Tristan -/ import SampCert.DifferentialPrivacy.Queries.BoundedMean.Basic import SampCert.DifferentialPrivacy.Queries.Histogram.Basic +import SampCert.DifferentialPrivacy.PermuteAndFlip.Basic import SampCert.DifferentialPrivacy.ZeroConcentrated.System import SampCert.DifferentialPrivacy.Pure.System import SampCert.DifferentialPrivacy.Queries.HistogramMean.Properties diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Basic.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Basic.lean new file mode 100644 index 00000000..322beb1f --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Basic.lean @@ -0,0 +1,43 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism +import SampCert.DifferentialPrivacy.PermuteAndFlip.Paper +import SampCert.DifferentialPrivacy.PermuteAndFlip.Reduction +import SampCert.DifferentialPrivacy.PermuteAndFlip.Privacy +import SampCert.DifferentialPrivacy.PermuteAndFlip.Peeling +import SampCert.DifferentialPrivacy.PermuteAndFlip.DPBridge + +/-! +Facade module for the permute-and-flip development. + +Paper-to-code map: +- Proposition 2 / regularity reduction: + [Reduction.reduced_privacy_of_regular](SampCert/DifferentialPrivacy/PermuteAndFlip/Reduction.lean) + (namespace `SLang.PermuteAndFlip.Reduction`) +- Closed-form PMF bridge used in the proof of Theorem 1: + [Paper.ClosedForm.permuteAndFlipPMF_eq_ofReal_paperProb_mul_paperAlt](SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/ClosedForm.lean) +- Regularity / monotonicity for permute-and-flip: + [Monotonicity.permuteAndFlipPMF_monotone](SampCert/DifferentialPrivacy/PermuteAndFlip/Monotonicity.lean) +- Final PMF privacy theorem: + [Privacy.permuteAndFlipPMF_range_privacy](SampCert/DifferentialPrivacy/PermuteAndFlip/Privacy.lean) +- Exact `SLang` refinement: + [Privacy.permuteAndFlipSLang_range_privacy](SampCert/DifferentialPrivacy/PermuteAndFlip/Privacy.lean) + +Main entry theorems: +- `permuteAndFlipPMF_range_privacy` +- `permuteAndFlipSLang_range_privacy` + +For implementation details, start with: +- `Mechanism` for the executable mechanism and its permutation-averaged PMF +- `Paper` for the paper-style PMF derivation +- `Range` for the range-distance metric layer +- `MonotonicityLocal` for the local bump/lower lemmas +- `Monotonicity` for the global monotonicity and privacy-step lemmas +- `Privacy` for the final exported privacy theorems +- `Reduction` for the standalone abstract regularity reduction (paper Proposition 2) +- `Peeling` for the peeling generalization of range-privacy composition +- `DPBridge` for the bridge from range-privacy to pure DP +-/ diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/DPBridge.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/DPBridge.lean new file mode 100644 index 00000000..1014d7b4 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/DPBridge.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Privacy +import SampCert.DifferentialPrivacy.Pure.DP +import Mathlib.Analysis.SpecialFunctions.Exp +import Mathlib.Data.ENNReal.Real + +noncomputable section + +open Classical + +namespace SLang +namespace PermuteAndFlip + +/-- Dataset-level wrapper around the verified PMF implementation of permute-and-flip. -/ +def scoreMechanismPMF {T : Type} {n : CandidateCount} + (score : List T → Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) : + SLang.Mechanism T (Fin n.succ) := + fun l => permuteAndFlipPMF n (score l) ε₁ ε₂ + +/-- The score map has range sensitivity `Δ` when neighbouring datasets induce +score vectors whose range distance is at most `Δ`. -/ +def rangeSensitive {T : Type} {n : CandidateCount} + (score : List T → Scores n) (Δ : ℕ) : Prop := + ∀ l₁ l₂ : List T, Neighbour l₁ l₂ → + rangeDistance (score l₁) (score l₂) ≤ Δ + +/-- +A helper inequality for turning the pointwise `rangeDistance` privacy theorem into +SampCert's ratio-style DP bound. +-/ +lemma privacy_multiplier_ge_one + (ε₁ : ℕ) (ε₂ : ℕ+) {d Δ : ℕ} (hd : d ≤ Δ) : + 1 ≤ + ENNReal.ofReal + (Real.exp ((((Δ : ℕ) : NNReal) * (((ε₁ : ℕ) : NNReal) / ε₂) : NNReal))) * + (privacyBase ε₁ ε₂) ^ d := by + let η : ℝ := ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) + have _hη : 0 ≤ η := by + positivity + have hrewrite : + ENNReal.ofReal (Real.exp ((Δ : ℝ) * η)) * (privacyBase ε₁ ε₂) ^ d = + ENNReal.ofReal (Real.exp ((Δ - d : ℕ) * η)) := by + calc + ENNReal.ofReal (Real.exp ((Δ : ℝ) * η)) * (privacyBase ε₁ ε₂) ^ d + = ENNReal.ofReal (Real.exp ((Δ : ℝ) * η)) * ENNReal.ofReal ((Real.exp (-η)) ^ d) := by + simp [privacyBase, η, ENNReal.ofReal_pow, Real.exp_nonneg] + _ = ENNReal.ofReal (Real.exp ((Δ : ℝ) * η) * (Real.exp (-η)) ^ d) := by + rw [← ENNReal.ofReal_mul] + positivity + _ = ENNReal.ofReal (Real.exp ((Δ : ℝ) * η) * Real.exp ((d : ℝ) * (-η))) := by + rw [← Real.exp_nat_mul] + _ = ENNReal.ofReal (Real.exp (((Δ : ℝ) * η) + ((d : ℝ) * (-η)))) := by + rw [← Real.exp_add] + _ = ENNReal.ofReal (Real.exp ((Δ - d : ℕ) * η)) := by + apply congrArg ENNReal.ofReal + apply congrArg Real.exp + calc + ((Δ : ℝ) * η) + ((d : ℝ) * (-η)) = (((Δ : ℝ) - d) * η) := by ring + _ = ((Δ - d : ℕ) : ℝ) * η := by rw [Nat.cast_sub hd] + have hreal : 1 ≤ Real.exp ((Δ - d : ℕ) * η) := by + calc + 1 = Real.exp 0 := by simp + _ ≤ Real.exp ((Δ - d : ℕ) * η) := by + apply Real.exp_le_exp.mpr + positivity + rw [show ENNReal.ofReal + (Real.exp ((((Δ : ℕ) : NNReal) * (((ε₁ : ℕ) : NNReal) / ε₂) : NNReal))) + = ENNReal.ofReal (Real.exp ((Δ : ℝ) * η)) by rfl] + rw [hrewrite] + exact ENNReal.one_le_ofReal.mpr hreal + +/-- +The permute-and-flip PMF wrapper satisfies SampCert's event-based `DP` definition +whenever the score function is range-sensitive on neighbouring datasets. +-/ +theorem permuteAndFlipPMF_DP_bound_of_rangeSensitive + {T : Type} {n : CandidateCount} + (score : List T → Scores n) (Δ : ℕ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hΔ : rangeSensitive score Δ) : + SLang.DP (scoreMechanismPMF score ε₁ ε₂) + (((Δ : ℕ) : NNReal) * (((ε₁ : ℕ) : NNReal) / ε₂)) := by + apply (SLang.event_eq_singleton _ _).mpr + intro l₁ l₂ hneigh r + let d := rangeDistance (score l₁) (score l₂) + let E : ENNReal := + ENNReal.ofReal + (Real.exp ((((Δ : ℕ) : NNReal) * (((ε₁ : ℕ) : NNReal) / ε₂) : NNReal))) + have hbase : + (privacyBase ε₁ ε₂) ^ d * scoreMechanismPMF score ε₁ ε₂ l₁ r + ≤ scoreMechanismPMF score ε₁ ε₂ l₂ r := by + simpa [scoreMechanismPMF, d] using + permuteAndFlipPMF_range_privacy + (q := score l₁) (q' := score l₂) (r := r) (ε₁ := ε₁) (ε₂ := ε₂) + have hd : d ≤ Δ := hΔ l₁ l₂ hneigh + have hscale : 1 ≤ E * (privacyBase ε₁ ε₂) ^ d := by + simpa [E, d] using privacy_multiplier_ge_one ε₁ ε₂ hd + have hmul : + scoreMechanismPMF score ε₁ ε₂ l₁ r + ≤ E * scoreMechanismPMF score ε₁ ε₂ l₂ r := by + calc + scoreMechanismPMF score ε₁ ε₂ l₁ r + = 1 * scoreMechanismPMF score ε₁ ε₂ l₁ r := by simp + _ ≤ (E * (privacyBase ε₁ ε₂) ^ d) * scoreMechanismPMF score ε₁ ε₂ l₁ r := by + exact mul_le_mul_left hscale _ + _ = E * ((privacyBase ε₁ ε₂) ^ d * scoreMechanismPMF score ε₁ ε₂ l₁ r) := by + ac_rfl + _ ≤ E * scoreMechanismPMF score ε₁ ε₂ l₂ r := by + exact mul_le_mul_right hbase E + exact ENNReal.div_le_of_le_mul hmul + +/-- +Pure-DP version of the range-sensitive bridge theorem for permute-and-flip. + +Since SampCert's neighboring definition is hardcoded, +this specializes the result to SampCert's definition of DP. +-/ +theorem permuteAndFlipPMF_PureDP_of_rangeSensitive + {T : Type} {n : CandidateCount} + (score : List T → Scores n) (Δ : ℕ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hΔ : rangeSensitive score Δ) : + SLang.PureDP (scoreMechanismPMF score ε₁ ε₂) + (((Δ : ℕ) : NNReal) * (((ε₁ : ℕ) : NNReal) / ε₂)) := by + exact permuteAndFlipPMF_DP_bound_of_rangeSensitive score Δ ε₁ ε₂ hΔ + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism.lean new file mode 100644 index 00000000..8b33754c --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism.Core +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism.SelectorCore +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism.Selector + +/-! +Reader-facing entry point for the executable permute-and-flip mechanism. + +Reading order: +- `Mechanism.Core` defines scores, gaps, the recursive selector core, and the exact sampler. +- `Mechanism.SelectorCore` proves selector-weight and canonical-order lemmas. +- `Mechanism.Selector` builds the permutation-averaged PMF and `SLang` mechanism. + +Key definitions and theorems: +- `permuteAndFlipPMF` +- `permuteAndFlipSLang` +- `permuteAndFlipSLang_eq_permuteAndFlipPMF` +- `permuteAndFlipPMF_eq_coin_mul_tsum_beforeSet_prod` +-/ diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/Core.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/Core.lean new file mode 100644 index 00000000..02ddf7e9 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/Core.lean @@ -0,0 +1,530 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.SLang +import SampCert.Samplers.BernoulliNegativeExponential.Basic +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Analysis.Calculus.Deriv.Pow +import Mathlib.Analysis.Calculus.MeanValue +import Mathlib.Analysis.Convex.Deriv +import Mathlib.Data.List.FinRange +import Mathlib.Data.Fintype.Lattice +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Probability.ProbabilityMassFunction.Constructions + +noncomputable section + +open scoped Classical +open PMF + +namespace SLang +namespace PermuteAndFlip +/-! +Core mechanism definitions and selector-level lemmas. + +Reading guide: +- first read the score transformations `bumpScore`, `lowerScore`, and `gap`; +- then `exactCoinPMF`, `selectPMFCore`, and `selectSLangCore`; +- finally the permutation and shift lemmas that later modules reuse. +-/ + +/-- We model the mechanism over a finite candidate set of size `n + 1`. -/ +abbrev CandidateCount := ℕ +/-- A score vector assigns a natural-valued score to each candidate. -/ +abbrev Scores (n : CandidateCount) := Fin n.succ → ℕ + +/-! ### Score transforms and gap algebra -/ + +/-- The maximum score in a finite score vector. -/ +def maxScore {n : CandidateCount} (q : Scores n) : ℕ := + Finset.sup Finset.univ q + +/-- Raise the distinguished candidate `r` by `k`. -/ +def bumpScore {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (k : ℕ) : Scores n := + fun i => q i + if i = r then k else 0 + +/-- Lower the distinguished candidate `r` by `k`, clipping at `0` in `ℕ`. -/ +def lowerScore {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (k : ℕ) : Scores n := + fun i => q i - if i = r then k else 0 + +theorem lowerScore_add {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (a b : ℕ) : + lowerScore (lowerScore q r a) r b = lowerScore q r (a + b) := by + funext i + by_cases hi : i = r + · subst hi + simp [lowerScore, Nat.sub_sub] + · simp [lowerScore, hi] + +def lowerOthersAlong {n : CandidateCount} + (l : List (Fin n.succ)) (q q' : Scores n) (r : Fin n.succ) : Scores n := + match l with + | [] => q + | s :: l => + if s = r then + lowerOthersAlong l q q' r + else + lowerOthersAlong l (lowerScore q s (q s - q' s)) q' r + +def permuteScores {n : CandidateCount} (τ : Equiv.Perm (Fin n.succ)) (q : Scores n) : Scores n := + fun i => q (τ.symm i) + +@[simp] +theorem probPure_apply_eq_pure_apply {α : Type} (a x : α) : + (probPure a : SLang α) x = PMF.pure a x := rfl + +/-- +`gap q i` is the amount by which `i` trails the current maximum. It is the key +quantity in permute-and-flip: the acceptance probability for `i` decays +exponentially in this gap. +-/ +def gap {n : CandidateCount} (q : Scores n) (i : Fin n.succ) : ℕ := + Finset.sup Finset.univ fun j => q j - q i + +theorem exists_argmax {n : CandidateCount} (q : Scores n) : + ∃ i : Fin n.succ, q i = maxScore q := by + obtain ⟨i, -, hi⟩ := Finset.exists_max_image Finset.univ q ⟨0, by simp⟩ + refine ⟨i, le_antisymm (Finset.le_sup (s := Finset.univ) (f := q) (by simp)) ?_⟩ + exact Finset.sup_le (fun j _ => hi j (by simp)) + +theorem gap_eq_maxScore_sub {n : CandidateCount} (q : Scores n) (i : Fin n.succ) : + gap q i = maxScore q - q i := by + -- The supremum over `j ↦ q j - q i` is attained at an argmax of `q`. + refine le_antisymm ?_ ?_ + · unfold gap maxScore + refine Finset.sup_le ?_ + intro j _ + exact Nat.sub_le_sub_right (Finset.le_sup (s := Finset.univ) (f := q) (by simp)) (q i) + · obtain ⟨m, hm⟩ := exists_argmax q + rw [← hm] + unfold gap + exact Finset.le_sup (s := Finset.univ) (f := fun j => q j - q i) (by simp) + +theorem maxScore_bumpScore_of_le {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (k : ℕ) (h : q r + k ≤ maxScore q) : + maxScore (bumpScore q r k) = maxScore q := by + -- If raising `r` still leaves it below the old maximum, then the maximum value + -- itself does not change. + refine le_antisymm ?_ ?_ + · unfold maxScore bumpScore + refine Finset.sup_le ?_ + intro i _ + by_cases hi : i = r + · subst hi + simpa using h + · simpa [hi] using Finset.le_sup (s := Finset.univ) (f := q) (by simp : i ∈ Finset.univ) + · obtain ⟨m, hm⟩ := exists_argmax q + rw [← hm] + unfold maxScore bumpScore + calc + q m ≤ q m + if m = r then k else 0 := by + by_cases hm' : m = r <;> simp [hm'] + _ ≤ Finset.sup Finset.univ (fun i => q i + if i = r then k else 0) := + Finset.le_sup (s := Finset.univ) (f := fun i => q i + if i = r then k else 0) (by simp) + +theorem gap_bumpScore_self_of_le {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (k : ℕ) (h : q r + k ≤ maxScore q) : + gap (bumpScore q r k) r = gap q r - k := by + rw [gap_eq_maxScore_sub, gap_eq_maxScore_sub, maxScore_bumpScore_of_le q r k h] + simp [bumpScore] + omega + +theorem gap_bumpScore_other_of_le {n : CandidateCount} + (q : Scores n) (r i : Fin n.succ) (k : ℕ) (hi : i ≠ r) (h : q r + k ≤ maxScore q) : + gap (bumpScore q r k) i = gap q i := by + rw [gap_eq_maxScore_sub, gap_eq_maxScore_sub, maxScore_bumpScore_of_le q r k h] + simp [bumpScore, hi] + +theorem maxScore_bumpScore_of_ge {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (k : ℕ) (h : maxScore q ≤ q r + k) : + maxScore (bumpScore q r k) = q r + k := by + -- Once `r` reaches or exceeds the old maximum, it becomes a maximizer in the + -- bumped score vector, so the new maximum is exactly its bumped score. + refine le_antisymm ?_ ?_ + · unfold maxScore bumpScore + refine Finset.sup_le ?_ + intro i _ + by_cases hi : i = r + · subst hi + simp + · have hqi : q i ≤ maxScore q := Finset.le_sup (s := Finset.univ) (f := q) (by simp) + calc + (q i + if i = r then k else 0) = q i := by simp [hi] + _ ≤ maxScore q := hqi + _ ≤ q r + k := h + · unfold maxScore bumpScore + simpa using + (Finset.le_sup (s := Finset.univ) (f := fun i => q i + if i = r then k else 0) (by simp : r ∈ Finset.univ)) + +theorem gap_bumpScore_self_of_ge {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (k : ℕ) (h : maxScore q ≤ q r + k) : + gap (bumpScore q r k) r = 0 := by + rw [gap_eq_maxScore_sub, maxScore_bumpScore_of_ge q r k h] + simp [bumpScore] + +theorem maxScore_eq_of_gap_zero {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (hgap : gap q r = 0) : + maxScore q = q r := by + rw [gap_eq_maxScore_sub] at hgap + exact le_antisymm (Nat.sub_eq_zero_iff_le.mp hgap) + (Finset.le_sup (s := Finset.univ) (f := q) (by simp)) + +theorem gap_bumpScore_other_of_gap_zero {n : CandidateCount} + (q : Scores n) (r i : Fin n.succ) (k : ℕ) (hi : i ≠ r) (hgap : gap q r = 0) : + gap (bumpScore q r k) i = gap q i + k := by + -- If `r` is already a maximizer, bumping `r` by `k` leaves every other score + -- unchanged but moves the maximum up by `k`, so every competing gap grows by `k`. + have hmax : maxScore q = q r := maxScore_eq_of_gap_zero q r hgap + have hle : q i ≤ q r := by + rw [← hmax] + exact Finset.le_sup (s := Finset.univ) (f := q) (by simp) + rw [gap_eq_maxScore_sub, gap_eq_maxScore_sub, maxScore_bumpScore_of_ge q r k] + · rw [hmax] + simp [bumpScore, hi] + omega + · simp [hmax] + +theorem bumpScore_add {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (k₁ k₂ : ℕ) : + bumpScore (bumpScore q r k₁) r k₂ = bumpScore q r (k₁ + k₂) := by + funext i + by_cases hi : i = r + · subst hi + simp [bumpScore, Nat.add_assoc] + · simp [bumpScore, hi] + +theorem gap_lowerScore_self_of_max_eq {n : CandidateCount} + (q : Scores n) (s : Fin n.succ) (k : ℕ) + (hk : k ≤ q s) + (hmax : maxScore (lowerScore q s k) = maxScore q) : + gap (lowerScore q s k) s = gap q s + k := by + rw [gap_eq_maxScore_sub, gap_eq_maxScore_sub, hmax] + simp [lowerScore] + have hs : q s - k + k = q s := Nat.sub_add_cancel hk + have hq : q s ≤ maxScore q := Finset.le_sup (s := Finset.univ) (f := q) (by simp) + omega + +theorem gap_lowerScore_other_of_max_eq {n : CandidateCount} + (q : Scores n) (s i : Fin n.succ) (k : ℕ) + (hi : i ≠ s) + (hmax : maxScore (lowerScore q s k) = maxScore q) : + gap (lowerScore q s k) i = gap q i := by + rw [gap_eq_maxScore_sub, gap_eq_maxScore_sub, hmax] + simp [lowerScore, hi] + +theorem maxScore_lowerScore_unique_max_one {n : CandidateCount} + (q : Scores n) (s : Fin n.succ) + (huniq : ∀ t : Fin n.succ, t ≠ s → q t < q s) : + maxScore (lowerScore q s 1) = q s - 1 := by + refine le_antisymm ?_ ?_ + · unfold maxScore lowerScore + refine Finset.sup_le ?_ + intro i + by_cases his : i = s + · subst his + simp + · have hlt : q i < q s := huniq i his + have hle : q i ≤ q s - 1 := Nat.le_pred_of_lt hlt + simpa [lowerScore, his] using hle + · unfold maxScore lowerScore + simpa [lowerScore] using + (Finset.le_sup (s := Finset.univ) + (f := fun i => q i - if i = s then 1 else 0) (by simp : s ∈ Finset.univ)) + +theorem maxScore_eq_of_unique_max {n : CandidateCount} + (q : Scores n) (s : Fin n.succ) + (huniq : ∀ t : Fin n.succ, t ≠ s → q t < q s) : + maxScore q = q s := by + apply le_antisymm + · refine Finset.sup_le ?_ + intro i _hi + by_cases his : i = s + · simp [his] + · exact le_of_lt (huniq i his) + · exact Finset.le_sup (s := Finset.univ) (f := q) (by simp) + +theorem gap_lowerScore_other_of_unique_max_one {n : CandidateCount} + (q : Scores n) (s i : Fin n.succ) + (hi : i ≠ s) + (huniq : ∀ t : Fin n.succ, t ≠ s → q t < q s) : + gap (lowerScore q s 1) i = gap q i - 1 := by + -- Lowering the unique maximizer by one decreases the maximum by one while + -- leaving the competing score `q i` untouched. + have hmax : maxScore (lowerScore q s 1) = q s - 1 := + maxScore_lowerScore_unique_max_one q s huniq + have hold : maxScore q = q s := maxScore_eq_of_unique_max q s huniq + rw [gap_eq_maxScore_sub, gap_eq_maxScore_sub, hmax, hold] + simp [lowerScore, hi] + have hlt : q i < q s := huniq i hi + omega + +@[simp] +theorem gap_shift {n : CandidateCount} (q : Scores n) (c : ℕ) (i : Fin n.succ) : + gap (fun j => q j + c) i = gap q i := by + unfold gap + refine Finset.sup_congr rfl ?_ + intro j _ + simp [Nat.add_sub_add_right] + +@[simp] +theorem gap_permute {n : CandidateCount} (τ : Equiv.Perm (Fin n.succ)) (q : Scores n) (i : Fin n.succ) : + gap (permuteScores τ q) (τ i) = gap q i := by + unfold gap permuteScores + apply le_antisymm + · refine Finset.sup_le ?_ + intro j _ + have h : + (fun k => q k - q i) (τ.symm j) ≤ + Finset.univ.sup (fun k => q k - q i) := + Finset.le_sup (s := Finset.univ) (f := fun k => q k - q i) (Finset.mem_univ (τ.symm j)) + simpa using h + · refine Finset.sup_le ?_ + intro j _ + have h : + (fun k => q (τ.symm k) - q (τ.symm (τ i))) (τ j) ≤ + Finset.univ.sup (fun k => q (τ.symm k) - q (τ.symm (τ i))) := + Finset.le_sup + (s := Finset.univ) + (f := fun k => q (τ.symm k) - q (τ.symm (τ i))) + (Finset.mem_univ (τ j)) + simpa using h + +theorem exists_gap_zero {n : CandidateCount} (q : Scores n) : + ∃ i : Fin n.succ, gap q i = 0 := by + obtain ⟨i, -, hi⟩ := Finset.exists_max_image Finset.univ q ⟨0, by simp⟩ + refine ⟨i, le_antisymm ?_ (Nat.zero_le _)⟩ + refine Finset.sup_le ?_ + intro j _ + exact Nat.sub_eq_zero_of_le (hi j (by simp)) ▸ Nat.zero_le 0 + +def exactCoinPMF (num : ℕ) (den : ℕ+) : PMF Bool := + PMF.bernoulli ⟨Real.exp (- ((num : NNReal) / den)), by positivity⟩ (by + have hnonneg : 0 ≤ ((num : NNReal) / den : ℝ) := by positivity + have hle : Real.exp (-((num : NNReal) / den : ℝ)) ≤ Real.exp 0 := by + exact Real.exp_le_exp.mpr (by linarith) + have h' : (⟨Real.exp (- ((num : NNReal) / den : ℝ)), by positivity⟩ : NNReal) ≤ 1 := by + change Real.exp (- ((num : NNReal) / den : ℝ)) ≤ 1 + simpa using hle + simpa using h') + +@[simp] +theorem exactCoinPMF_apply_true (num : ℕ) (den : ℕ+) : + exactCoinPMF num den true = ENNReal.ofReal (Real.exp (- ((num : NNReal) / den))) := by + simp [exactCoinPMF] + simpa using + (ENNReal.coe_nnreal_eq (⟨Real.exp (- ((num : NNReal) / den : ℝ)), by positivity⟩ : NNReal)) + +@[simp] +theorem exactCoinPMF_zero_apply_true (den : ℕ+) : + exactCoinPMF 0 den true = 1 := by + rw [exactCoinPMF_apply_true] + simp + +@[simp] +theorem exactCoinPMF_apply_false (num : ℕ) (den : ℕ+) : + exactCoinPMF num den false = 1 - ENNReal.ofReal (Real.exp (- ((num : NNReal) / den))) := by + simp [exactCoinPMF] + congr 1 + simpa using + (ENNReal.coe_nnreal_eq (⟨Real.exp (- ((num : NNReal) / den : ℝ)), by positivity⟩ : NNReal)) + +@[simp] +theorem exactCoinPMF_zero_apply_false (den : ℕ+) : + exactCoinPMF 0 den false = 0 := by + rw [exactCoinPMF_apply_false] + simp + +theorem exactCoinPMF_true_mul_exactCoinPMF_true + (a b : ℕ) (den : ℕ+) : + ENNReal.ofReal (Real.exp (- ((a : NNReal) / den))) * exactCoinPMF b den true = + exactCoinPMF (a + b) den true := by + -- Multiplying two exact exponential factors adds their exponents. + rw [exactCoinPMF_apply_true, exactCoinPMF_apply_true] + rw [← ENNReal.ofReal_mul] + · congr 1 + rw [← Real.exp_add] + have hden : (((den : NNReal) : ℝ)) ≠ 0 := by positivity + have hsum : + - ((a : NNReal) / den : ℝ) + - ((b : NNReal) / den : ℝ) = + - (((a + b : ℕ) : NNReal) / den : ℝ) := by + field_simp [hden] + ring_nf + simp [Nat.cast_add] + ring + exact congrArg Real.exp hsum + · positivity + +theorem exactCoinPMF_false_mono + (a b : ℕ) (den : ℕ+) (hab : a ≤ b) : + exactCoinPMF a den false ≤ exactCoinPMF b den false := by + -- The rejection probability `1 - exp(-x)` is monotone increasing in `x`. + rw [exactCoinPMF_apply_false, exactCoinPMF_apply_false] + apply tsub_le_tsub_left + apply ENNReal.ofReal_le_ofReal + have hab' : ((a : NNReal) : ℝ) ≤ ((b : NNReal) : ℝ) := by exact_mod_cast hab + have hden : (0 : ℝ) ≤ ((den : NNReal) : ℝ) := by positivity + have hdiv : (((a : NNReal) / den : NNReal) : ℝ) ≤ (((b : NNReal) / den : NNReal) : ℝ) := by + exact div_le_div_of_nonneg_right hab' hden + have hneg : -((((b : NNReal) / den : NNReal) : ℝ)) ≤ -((((a : NNReal) / den : NNReal) : ℝ)) := by + linarith + exact Real.exp_le_exp.mpr hneg + +theorem bernoulliExpNegSample_eq_exactCoinPMF (num : ℕ) (den : ℕ+) : + (BernoulliExpNegSample num den : SLang Bool) = exactCoinPMF num den := by + ext b + cases b + · rw [BernoulliExpNegSample_apply_false, exactCoinPMF_apply_false] + simp + · rw [BernoulliExpNegSample_apply_true, exactCoinPMF_apply_true] + simp + +def selectPMFCore {n : CandidateCount} : + List (Fin n.succ) → Scores n → ℕ → ℕ+ → PMF (Option (Fin n.succ)) + | [], _, _, _ => PMF.pure none + | i :: is, q, ε₁, ε₂ => do + -- Sample the exact Bernoulli test for the current candidate `i`. + let b ← exactCoinPMF (gap q i * ε₁) ε₂ + if b then + -- Accept immediately and stop scanning. + PMF.pure (some i) + else + -- Otherwise continue with the remaining candidates. + selectPMFCore is q ε₁ ε₂ + +def collapseOptionPMF {α : Type} [Inhabited α] (p : PMF (Option α)) : PMF α := + p.bind fun o => + match o with + | some a => PMF.pure a + -- This fallback is only used for the raw recursive selector. Later lemmas + -- show it has zero mass on the full candidate list. + | none => PMF.pure default + +def selectPMF {n : CandidateCount} : List (Fin n.succ) → Scores n → ℕ → ℕ+ → PMF (Fin n.succ) + | l, q, ε₁, ε₂ => collapseOptionPMF (selectPMFCore l q ε₁ ε₂) + +def selectSLangCore {n : CandidateCount} : + List (Fin n.succ) → Scores n → ℕ → ℕ+ → SLang (Option (Fin n.succ)) + | [], _, _, _ => return none + | i :: is, q, ε₁, ε₂ => do + let b ← BernoulliExpNegSample (gap q i * ε₁) ε₂ + if b then + return some i + else + selectSLangCore is q ε₁ ε₂ + +def collapseOptionSLang {α : Type} [Inhabited α] (p : SLang (Option α)) : SLang α := do + let o ← p + match o with + | some a => return a + | none => return default + +def selectSLang {n : CandidateCount} : List (Fin n.succ) → Scores n → ℕ → ℕ+ → SLang (Fin n.succ) + | l, q, ε₁, ε₂ => collapseOptionSLang (selectSLangCore l q ε₁ ε₂) + +@[simp] +theorem selectSLangCore_eq_selectPMFCore {n : CandidateCount} + (l : List (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) : + selectSLangCore l q ε₁ ε₂ = selectPMFCore l q ε₁ ε₂ := by + induction l with + | nil => + ext i + simp [selectSLangCore, selectPMFCore] + | cons a l ih => + ext i + unfold selectSLangCore selectPMFCore + rw [bernoulliExpNegSample_eq_exactCoinPMF] + apply tsum_congr + intro b + by_cases hb : b = true + · subst hb + simp + · simp [hb, ih] + +@[simp] +theorem selectSLang_eq_selectPMF {n : CandidateCount} + (l : List (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) : + selectSLang l q ε₁ ε₂ = selectPMF l q ε₁ ε₂ := by + ext i + simp [selectSLang, selectPMF, collapseOptionSLang, collapseOptionPMF, selectSLangCore_eq_selectPMFCore] + +@[simp] +theorem selectPMFCore_permute {n : CandidateCount} + (τ : Equiv.Perm (Fin n.succ)) (l : List (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) + (o : Option (Fin n.succ)) : + selectPMFCore (l.map τ) (permuteScores τ q) ε₁ ε₂ (o.map τ) = selectPMFCore l q ε₁ ε₂ o := by + induction l with + | nil => + cases o <;> simp [selectPMFCore] + | cons a l ih => + cases o with + | none => + unfold selectPMFCore + simp [gap_permute] + simpa using + congrArg + (fun t => (1 - ENNReal.ofReal (Real.exp (-((gap q a * ε₁ : NNReal) / ε₂)))) * t) ih + | some r => + unfold selectPMFCore + simp [gap_permute] + simpa using + congrArg + (fun t => + (if r = a then ENNReal.ofReal (Real.exp (-((gap q a * ε₁ : NNReal) / ε₂))) else 0) + + (1 - ENNReal.ofReal (Real.exp (-((gap q a * ε₁ : NNReal) / ε₂)))) * t) ih + +@[simp] +theorem selectPMFCore_shift {n : CandidateCount} + (l : List (Fin n.succ)) (q : Scores n) (c ε₁ : ℕ) (ε₂ : ℕ+) : + selectPMFCore l (fun j => q j + c) ε₁ ε₂ = selectPMFCore l q ε₁ ε₂ := by + induction l with + | nil => + simp [selectPMFCore] + | cons a l ih => + simp [selectPMFCore, gap_shift, ih] + +theorem selectPMFCore_none_of_gap_zero {n : CandidateCount} + (l : List (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) + {i : Fin n.succ} (hi : i ∈ l) (hgap : gap q i = 0) : + selectPMFCore l q ε₁ ε₂ none = 0 := by + revert i + induction l with + | nil => + intro i hi + cases hi + | cons a l ih => + intro i hi hgap + simp at hi + rcases hi with rfl | hi + · unfold selectPMFCore + simp [hgap] + · unfold selectPMFCore + have ih' := ih hi hgap + by_cases hb : gap q a * ε₁ = 0 + · simp [hb] + · simp [ih'] + +theorem selectPMFCore_some_eq_zero_of_not_mem {n : CandidateCount} + (l : List (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) + {r : Fin n.succ} (hr : r ∉ l) : + selectPMFCore l q ε₁ ε₂ (some r) = 0 := by + induction l with + | nil => + simp [selectPMFCore] + | cons a l ih => + have hra : r ≠ a := by + intro h + apply hr + simp [h] + have hrtail : r ∉ l := by + intro h + apply hr + simp [h] + unfold selectPMFCore + by_cases hb : exactCoinPMF (gap q a * ε₁) ε₂ true = 0 + · simp [PMF.bind_apply, hb, hra, ih hrtail] + · simp [PMF.bind_apply, hra, ih hrtail] + + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/Selector.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/Selector.lean new file mode 100644 index 00000000..746e41d0 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/Selector.lean @@ -0,0 +1,131 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism.SelectorCore + +noncomputable section + +open scoped Classical +open PMF + +namespace SLang +namespace PermuteAndFlip +/-! +Permutation-averaged mechanism definitions built on top of selector-core lemmas. +-/ + +/-- +The PMF-level permute-and-flip mechanism: draw a uniform random permutation of +the candidates, then run the fixed-order selector on that order. +-/ +def permuteAndFlipPMF (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) : + PMF (Fin n.succ) := do + let σ ← PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ + +/-- +The executable `SLang` implementation of permute-and-flip, using the same +uniform permutation plus exact Bernoulli-exponential selector. +-/ +def permuteAndFlipSLang (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) : + SLang (Fin n.succ) := do + let σ ← ((PMF.uniformOfFintype (Equiv.Perm (Fin n.succ))) : SLang (Equiv.Perm (Fin n.succ))) + selectSLang ((canonicalOrder n).map σ) q ε₁ ε₂ + +@[simp] +theorem permuteAndFlipSLang_eq_permuteAndFlipPMF + (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) : + permuteAndFlipSLang n q ε₁ ε₂ = permuteAndFlipPMF n q ε₁ ε₂ := by + ext i + simp [permuteAndFlipSLang, permuteAndFlipPMF, selectSLang_eq_selectPMF] + +@[simp] +theorem permuteAndFlipPMF_permute + (n : CandidateCount) (τ : Equiv.Perm (Fin n.succ)) (q : Scores n) + (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + permuteAndFlipPMF n (permuteScores τ q) ε₁ ε₂ (τ r) = + permuteAndFlipPMF n q ε₁ ε₂ r := by + -- Reindex the uniform sum over permutations by right-composition with `τ`. + let e : Equiv.Perm (Equiv.Perm (Fin n.succ)) := + { toFun := fun σ => σ.trans τ + invFun := fun σ => σ.trans τ.symm + left_inv := by + intro σ + ext x + simp + right_inv := by + intro σ + ext x + simp } + simp [permuteAndFlipPMF, PMF.bind_apply] + conv_lhs => rw [← Equiv.sum_comp e] + apply Fintype.sum_congr + intro σ + simpa [e, Function.comp, PMF.uniformOfFintype_apply] using + congrArg (fun x => (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) (e σ)) * x) + (selectPMF_map_canonicalOrder_permute σ τ q ε₁ ε₂ r) + +theorem permuteAndFlipPMF_eq_tsum_selectWeight + (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + permuteAndFlipPMF n q ε₁ ε₂ r = + ∑' σ : Equiv.Perm (Fin n.succ), + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + selectWeight ((canonicalOrder n).map σ) q ε₁ ε₂ r := by + -- Unfold the `bind` in `permuteAndFlipPMF` and replace the + -- fixed-order selector PMF with the explicit weight formula from + -- `SelectorCore`. + simp [permuteAndFlipPMF, PMF.bind_apply, selectPMF_map_canonicalOrder_eq_selectWeight] + +/-- +This is the first closed form used later in the paper proof: factor out the +success probability of `r`, and average only the failure products over +candidates that appear before `r` in the sampled permutation. + +This theorem is the executable-mechanism counterpart of the permutation-average formula +used in the paper's supplement before the inclusion-exclusion rewrite. +-/ +theorem permuteAndFlipPMF_eq_coin_mul_tsum_beforeSet_prod + (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + permuteAndFlipPMF n q ε₁ ε₂ r = + exactCoinPMF (gap q r * ε₁) ε₂ true * + ∑' σ : Equiv.Perm (Fin n.succ), + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + Finset.prod (beforeSet σ r) (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false) := by + rw [permuteAndFlipPMF_eq_tsum_selectWeight] + calc + ∑' σ : Equiv.Perm (Fin n.succ), + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + selectWeight ((canonicalOrder n).map σ) q ε₁ ε₂ r + = + ∑' σ : Equiv.Perm (Fin n.succ), + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + (exactCoinPMF (gap q r * ε₁) ε₂ true * + Finset.prod (beforeSet σ r) (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false)) := by + -- Replace the fixed-order selector weight by its prefix-product formula. + refine tsum_congr (fun σ => ?_) + exact congrArg + (fun x => PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * x) + (by + simpa [canonicalOrder] using + selectWeight_map_finRange_eq_coin_mul_beforeSet_prod σ q r ε₁ ε₂) + _ = + ∑' σ : Equiv.Perm (Fin n.succ), + exactCoinPMF (gap q r * ε₁) ε₂ true * + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + Finset.prod (beforeSet σ r) (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false)) := by + refine tsum_congr (fun σ => ?_) + ac_rfl + _ = + exactCoinPMF (gap q r * ε₁) ε₂ true * + ∑' σ : Equiv.Perm (Fin n.succ), + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + Finset.prod (beforeSet σ r) (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false) := by + -- The factor involving `r` is independent of the sampled + -- permutation, so it can be pulled completely outside the sum. + rw [ENNReal.tsum_mul_left] + + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/SelectorCore.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/SelectorCore.lean new file mode 100644 index 00000000..b82ba2c0 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Mechanism/SelectorCore.lean @@ -0,0 +1,383 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Paper.Counting + +noncomputable section + +open scoped Classical +open PMF + +namespace SLang +namespace PermuteAndFlip +/-! +Selector-weight and canonical-order lemmas for the executable selector. + +Reading guide: +- `selectWeight` is the fixed-order probability of first accepting `r`; +- the `selectPMF...` lemmas connect that closed form back to the executable selector; +- the final lemmas lift fixed-order facts to canonical candidate orders. +-/ + +/-! ### Fixed-order selector weights -/ + +/-- +`selectWeight l q ... r` is the probability that a fixed scan order `l` +returns `r`: every earlier candidate must fail its Bernoulli test, and `r` +must succeed when first encountered. +-/ +def selectWeight {n : CandidateCount} : + List (Fin n.succ) → Scores n → ℕ → ℕ+ → Fin n.succ → ENNReal + | [], _, _, _, _ => 0 + | i :: is, q, ε₁, ε₂, r => + if i = r then + exactCoinPMF (gap q i * ε₁) ε₂ true + else + exactCoinPMF (gap q i * ε₁) ε₂ false * selectWeight is q ε₁ ε₂ r + +theorem selectWeight_eq_prefix_prod + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) (hr : r ∈ l) : + selectWeight l q ε₁ ε₂ r = + ((l.take (l.idxOf r)).map (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false)).prod * + exactCoinPMF (gap q r * ε₁) ε₂ true := by + induction l with + | nil => + cases hr + | cons a l ih => + simp at hl + rcases hl with ⟨ha, hnodup⟩ + simp at hr + rcases hr with rfl | hr + · simp [selectWeight, List.idxOf_cons_self] + · have har : a ≠ r := by + intro h + apply ha + simpa [h] using hr + rw [show selectWeight (a :: l) q ε₁ ε₂ r = + exactCoinPMF (gap q a * ε₁) ε₂ false * selectWeight l q ε₁ ε₂ r by + simp [selectWeight, har]] + rw [ih hnodup hr] + simp [har] + ac_rfl + +theorem selectWeight_map_finRange_eq_coin_mul_beforeSet_prod + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) + (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + selectWeight ((List.finRange n.succ).map σ) q ε₁ ε₂ r = + exactCoinPMF (gap q r * ε₁) ε₂ true * + Finset.prod (beforeSet σ r) (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false) := by + have hnodup : (((List.finRange n.succ).map σ).Nodup) := by + simpa using (List.nodup_finRange n.succ).map σ.injective + have hr : r ∈ ((List.finRange n.succ).map σ) := by + exact List.mem_map.mpr ⟨σ.symm r, by simp, by simp⟩ + rw [selectWeight_eq_prefix_prod ((List.finRange n.succ).map σ) hnodup q ε₁ ε₂ r hr] + have hprod : + (List.map (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false) + (List.take (((List.finRange n.succ).map σ).idxOf r) ((List.finRange n.succ).map σ))).prod + = Finset.prod (beforeSet σ r) (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false) := by + simpa only [List.ofFn_eq_map, indexOf_map_canonicalOrder] using + (prefix_prod_eq_beforeSet_prod σ r (fun i => exactCoinPMF (gap q i * ε₁) ε₂ false)) + rw [hprod] + ac_rfl + +/-! ### Connecting the recursive selector to the closed form -/ + +theorem selectPMFCore_cons_eq_head_of_not_mem {n : CandidateCount} + (a : Fin n.succ) (l : List (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) + (ha : a ∉ l) : + selectPMFCore (a :: l) q ε₁ ε₂ (some a) = exactCoinPMF (gap q a * ε₁) ε₂ true := by + simp [selectPMFCore, PMF.bind_apply, selectPMFCore_some_eq_zero_of_not_mem l q ε₁ ε₂ ha] + +theorem selectPMFCore_cons_eq_tail_of_ne {n : CandidateCount} + (a r : Fin n.succ) (l : List (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) + (har : r ≠ a) : + selectPMFCore (a :: l) q ε₁ ε₂ (some r) = + exactCoinPMF (gap q a * ε₁) ε₂ false * selectPMFCore l q ε₁ ε₂ (some r) := by + simp [selectPMFCore, PMF.bind_apply, har] + +@[simp] +theorem selectPMFCore_eq_selectWeight + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) + (r : Fin n.succ) : + selectPMFCore l q ε₁ ε₂ (some r) = selectWeight l q ε₁ ε₂ r := by + induction l with + | nil => + simp [selectPMFCore, selectWeight] + | cons a l ih => + simp at hl + rcases hl with ⟨ha, hnodup⟩ + by_cases har : r = a + · subst r + rw [selectPMFCore_cons_eq_head_of_not_mem a l q ε₁ ε₂ ha] + simp [selectWeight] + · rw [selectPMFCore_cons_eq_tail_of_ne a r l q ε₁ ε₂ har] + have hne : a ≠ r := by + intro h + exact har h.symm + simp [selectWeight, hne, ih hnodup] + +theorem selectWeight_bumpScore_self_of_gap_zero_le + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hr : r ∈ l) (hgap : gap q r = 0) : + selectWeight l q ε₁ ε₂ r ≤ + selectWeight l (bumpScore q r k) ε₁ ε₂ r := by + induction l generalizing q with + | nil => + cases hr + | cons a l ih => + simp at hl + rcases hl with ⟨ha, hnodup⟩ + simp at hr + rcases hr with h_eq | hr + · subst h_eq + -- If `r` is the head of the list, the selector weight is just the + -- acceptance probability for `r`, which only goes up after a bump. + have hmax : maxScore q ≤ q r + k := by + rw [maxScore_eq_of_gap_zero q r hgap] + exact Nat.le_add_right (q r) k + rw [show selectWeight (r :: l) q ε₁ ε₂ r = exactCoinPMF (gap q r * ε₁) ε₂ true by + simp [selectWeight]] + rw [show selectWeight (r :: l) (bumpScore q r k) ε₁ ε₂ r = + exactCoinPMF (gap (bumpScore q r k) r * ε₁) ε₂ true by + simp [selectWeight]] + rw [hgap, gap_bumpScore_self_of_ge q r k hmax] + · have har : r ≠ a := by + intro h + apply ha + simpa [h] using hr + have hne : a ≠ r := har.symm + -- Otherwise compare the head rejection probabilities and recurse on the tail. + rw [show selectWeight (a :: l) q ε₁ ε₂ r = + exactCoinPMF (gap q a * ε₁) ε₂ false * selectWeight l q ε₁ ε₂ r by + simp [selectWeight, hne]] + rw [show selectWeight (a :: l) (bumpScore q r k) ε₁ ε₂ r = + exactCoinPMF (gap (bumpScore q r k) a * ε₁) ε₂ false * + selectWeight l (bumpScore q r k) ε₁ ε₂ r by + simp [selectWeight, hne]] + have hcoin : + exactCoinPMF (gap q a * ε₁) ε₂ false ≤ + exactCoinPMF (gap (bumpScore q r k) a * ε₁) ε₂ false := by + apply exactCoinPMF_false_mono + rw [gap_bumpScore_other_of_gap_zero q r a k har.symm hgap] + exact Nat.mul_le_mul_right ε₁ (Nat.le_add_right (gap q a) k) + exact mul_le_mul' hcoin (ih hnodup q hr hgap) + +theorem selectWeight_lowerScore_other_of_max_eq_le + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q : Scores n) (r s : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) (hr : r ∈ l) (hk : k ≤ q s) + (hmax : maxScore (lowerScore q s k) = maxScore q) : + selectWeight l q ε₁ ε₂ r ≤ + selectWeight l (lowerScore q s k) ε₁ ε₂ r := by + induction l generalizing q with + | nil => + cases hr + | cons a l ih => + simp at hl + rcases hl with ⟨ha, hnodup⟩ + simp at hr + rcases hr with h_eq | hr + · subst h_eq + -- If `r` is at the head, lowering some other candidate can only improve + -- `r`'s head acceptance probability, provided the maximum stays fixed. + rw [show selectWeight (r :: l) q ε₁ ε₂ r = exactCoinPMF (gap q r * ε₁) ε₂ true by + simp [selectWeight]] + rw [show selectWeight (r :: l) (lowerScore q s k) ε₁ ε₂ r = + exactCoinPMF (gap (lowerScore q s k) r * ε₁) ε₂ true by + simp [selectWeight]] + rw [gap_lowerScore_other_of_max_eq q s r k hrs hmax] + · have har : r ≠ a := by + intro h + apply ha + simpa [h] using hr + have hne : a ≠ r := har.symm + -- If `r` is later in the list, compare the head rejection factor and then recurse. + rw [show selectWeight (a :: l) q ε₁ ε₂ r = + exactCoinPMF (gap q a * ε₁) ε₂ false * selectWeight l q ε₁ ε₂ r by + simp [selectWeight, hne]] + rw [show selectWeight (a :: l) (lowerScore q s k) ε₁ ε₂ r = + exactCoinPMF (gap (lowerScore q s k) a * ε₁) ε₂ false * + selectWeight l (lowerScore q s k) ε₁ ε₂ r by + simp [selectWeight, hne]] + have hcoin : + exactCoinPMF (gap q a * ε₁) ε₂ false ≤ + exactCoinPMF (gap (lowerScore q s k) a * ε₁) ε₂ false := by + by_cases has : a = s + · subst has + apply exactCoinPMF_false_mono + rw [gap_lowerScore_self_of_max_eq q a k (by simpa using hk) hmax] + exact Nat.mul_le_mul_right ε₁ (Nat.le_add_right (gap q a) k) + · apply le_of_eq + rw [gap_lowerScore_other_of_max_eq q s a k has hmax] + have htail : + selectWeight l q ε₁ ε₂ r ≤ + selectWeight l (lowerScore q s k) ε₁ ε₂ r := by + simpa using (ih hnodup (q := q) hr hk hmax) + exact mul_le_mul' hcoin htail + +theorem selectPMFCore_bumpScore_self_of_le + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hr : r ∈ l) (hmax : q r + k ≤ maxScore q) : + ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + selectPMFCore l (bumpScore q r k) ε₁ ε₂ (some r) = + selectPMFCore l q ε₁ ε₂ (some r) := by + induction l generalizing q with + | nil => + cases hr + | cons a l ih => + simp at hl + rcases hl with ⟨ha, hnodup⟩ + simp at hr + rcases hr with h_eq | hr + · subst h_eq + -- If `r` appears first, the desired equality is exactly the multiplicative + -- exponential identity for the head Bernoulli coin. + rw [selectPMFCore_cons_eq_head_of_not_mem r l (bumpScore q r k) ε₁ ε₂ ha] + rw [selectPMFCore_cons_eq_head_of_not_mem r l q ε₁ ε₂ ha] + have hk : k ≤ gap q r := by + rw [gap_eq_maxScore_sub] + omega + have hgap : gap (bumpScore q r k) r * ε₁ + k * ε₁ = gap q r * ε₁ := by + rw [gap_bumpScore_self_of_le q r k hmax] + calc + (gap q r - k) * ε₁ + k * ε₁ = ((gap q r - k) + k) * ε₁ := by + rw [Nat.add_mul] + _ = gap q r * ε₁ := by rw [Nat.sub_add_cancel hk] + rw [← hgap] + simpa [Nat.add_comm] using + exactCoinPMF_true_mul_exactCoinPMF_true (k * ε₁) (gap (bumpScore q r k) r * ε₁) ε₂ + · have har : r ≠ a := by + intro h + apply ha + simpa [h] using hr + -- If the head is some other candidate, its rejection probability is unchanged, + -- so the statement reduces to the induction hypothesis on the tail. + rw [selectPMFCore_cons_eq_tail_of_ne a r l (bumpScore q r k) ε₁ ε₂ har] + rw [selectPMFCore_cons_eq_tail_of_ne a r l q ε₁ ε₂ har] + rw [gap_bumpScore_other_of_le q r a k har.symm hmax] + calc + ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + (exactCoinPMF (gap q a * ε₁) ε₂ false * selectPMFCore l (bumpScore q r k) ε₁ ε₂ (some r)) + = exactCoinPMF (gap q a * ε₁) ε₂ false * + (ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + selectPMFCore l (bumpScore q r k) ε₁ ε₂ (some r)) := by + ac_rfl + _ = exactCoinPMF (gap q a * ε₁) ε₂ false * selectPMFCore l q ε₁ ε₂ (some r) := by + exact congrArg (fun x => exactCoinPMF (gap q a * ε₁) ε₂ false * x) (ih hnodup q hr hmax) + +def canonicalOrder (n : CandidateCount) : List (Fin n.succ) := + List.finRange n.succ + +theorem collapseOptionPMF_apply_of_none_zero {α : Type} [Inhabited α] + (p : PMF (Option α)) (hp : p none = 0) (a : α) : + collapseOptionPMF p a = p (some a) := by + unfold collapseOptionPMF + rw [PMF.bind_apply] + refine (tsum_eq_single (some a) ?_).trans ?_ + · intro x hx + cases x with + | none => + simp [hp] + | some b => + have hb : b ≠ a := by + intro h + apply hx + simp [h] + by_cases hab : a = b + · exfalso + exact hb hab.symm + · simp [PMF.pure_apply, hab] + · simp + +theorem selectPMF_eq_selectPMFCore_map_canonicalOrder {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r = + selectPMFCore ((canonicalOrder n).map σ) q ε₁ ε₂ (some r) := by + obtain ⟨i, hi⟩ := exists_gap_zero q + have hnone : + selectPMFCore ((canonicalOrder n).map σ) q ε₁ ε₂ none = 0 := by + -- On the full candidate list there is always some gap-zero candidate, so the + -- recursive selector never falls off the end without accepting someone. + exact selectPMFCore_none_of_gap_zero ((canonicalOrder n).map σ) q ε₁ ε₂ (by + exact List.mem_map.mpr ⟨σ.symm i, by simp [canonicalOrder], by simp⟩) hi + simp [selectPMF, collapseOptionPMF_apply_of_none_zero, hnone] + +/-! ### Canonical-order lifting lemmas -/ + +theorem selectPMF_map_canonicalOrder_eq_selectWeight {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r = + selectWeight ((canonicalOrder n).map σ) q ε₁ ε₂ r := by + rw [selectPMF_eq_selectPMFCore_map_canonicalOrder σ q ε₁ ε₂ r] + exact selectPMFCore_eq_selectWeight + ((canonicalOrder n).map σ) + (by simpa [canonicalOrder] using (List.nodup_finRange n.succ).map σ.injective) + q ε₁ ε₂ r + +theorem selectPMF_map_canonicalOrder_permute {n : CandidateCount} + (σ τ : Equiv.Perm (Fin n.succ)) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + selectPMF ((canonicalOrder n).map (σ.trans τ)) (permuteScores τ q) ε₁ ε₂ (τ r) = + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r := by + rw [selectPMF_eq_selectPMFCore_map_canonicalOrder (σ.trans τ) (permuteScores τ q) ε₁ ε₂ (τ r)] + rw [selectPMF_eq_selectPMFCore_map_canonicalOrder σ q ε₁ ε₂ r] + simpa [List.map_map] using + selectPMFCore_permute τ ((canonicalOrder n).map σ) q ε₁ ε₂ (some r) + +theorem selectPMF_bumpScore_self_of_le_map_canonicalOrder + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) + (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hmax : q r + k ≤ maxScore q) : + ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + selectPMF ((canonicalOrder n).map σ) (bumpScore q r k) ε₁ ε₂ r = + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r := by + rw [selectPMF_eq_selectPMFCore_map_canonicalOrder σ (bumpScore q r k) ε₁ ε₂ r] + rw [selectPMF_eq_selectPMFCore_map_canonicalOrder σ q ε₁ ε₂ r] + exact selectPMFCore_bumpScore_self_of_le + (((canonicalOrder n).map σ)) + (by + simpa [canonicalOrder] using (List.nodup_finRange n.succ).map σ.injective) + q r k ε₁ ε₂ + (by + exact List.mem_map.mpr ⟨σ.symm r, by simp [canonicalOrder], by simp⟩) + hmax + +theorem selectPMF_bumpScore_self_of_gap_zero_le_map_canonicalOrder + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) + (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hgap : gap q r = 0) : + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r ≤ + selectPMF ((canonicalOrder n).map σ) (bumpScore q r k) ε₁ ε₂ r := by + rw [selectPMF_map_canonicalOrder_eq_selectWeight σ q ε₁ ε₂ r] + rw [selectPMF_map_canonicalOrder_eq_selectWeight σ (bumpScore q r k) ε₁ ε₂ r] + exact selectWeight_bumpScore_self_of_gap_zero_le + (((canonicalOrder n).map σ)) + (by simpa [canonicalOrder] using (List.nodup_finRange n.succ).map σ.injective) + q r k ε₁ ε₂ + (by exact List.mem_map.mpr ⟨σ.symm r, by simp [canonicalOrder], by simp⟩) + hgap + +theorem selectPMF_lowerScore_other_of_max_eq_le_map_canonicalOrder + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) + (q : Scores n) (r s : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) (hk : k ≤ q s) + (hmax : maxScore (lowerScore q s k) = maxScore q) : + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r ≤ + selectPMF ((canonicalOrder n).map σ) (lowerScore q s k) ε₁ ε₂ r := by + rw [selectPMF_map_canonicalOrder_eq_selectWeight σ q ε₁ ε₂ r] + rw [selectPMF_map_canonicalOrder_eq_selectWeight σ (lowerScore q s k) ε₁ ε₂ r] + exact selectWeight_lowerScore_other_of_max_eq_le + (((canonicalOrder n).map σ)) + (by simpa [canonicalOrder] using (List.nodup_finRange n.succ).map σ.injective) + q r s k ε₁ ε₂ + hrs + (by exact List.mem_map.mpr ⟨σ.symm r, by simp [canonicalOrder], by simp⟩) + hk + hmax +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Monotonicity.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Monotonicity.lean new file mode 100644 index 00000000..1d66e9ef --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Monotonicity.lean @@ -0,0 +1,162 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.MonotonicityLocal + +/-! +Monotonicity and privacy-step lemmas for permute-and-flip. + +Reading order: +- `MonotonicityLocal` proves one-coordinate bump/lower lemmas. +- This file packages those into global shift invariance and monotonicity. +- It then derives the one-step and `k`-step privacy contractions used by + [Privacy](SampCert/DifferentialPrivacy/PermuteAndFlip/Privacy.lean). +-/ + +noncomputable section + +namespace SLang +namespace PermuteAndFlip + +section Global + +/-- +Adding the same constant to every score does not change permute-and-flip. +This shift-invariance is used in the privacy proof to normalize +integer score differences back into natural-valued score vectors. +-/ +theorem permuteAndFlipPMF_shift + {n : CandidateCount} (q : Scores n) (c ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + permuteAndFlipPMF n (fun i => q i + c) ε₁ ε₂ r = + permuteAndFlipPMF n q ε₁ ε₂ r := by + unfold permuteAndFlipPMF + -- The outer permutation average is unchanged; only the inner selector sees + -- the shifted scores, and `selectPMFCore_shift` already proved that the + -- selector depends only on score differences. + apply tsum_congr + intro σ + simp [selectPMF, selectPMFCore_shift] + +/-- +Global monotonicity: increasing the selected candidate and/or decreasing every +other candidate can only increase the probability of outputting `r`. + +The proof first bumps `r` up to its target score and then lowers the remaining +coordinates one by one using `lowerOthersAlong`. + +This is the concrete regularity/monotonicity condition corresponding to the +paper's regularity lemma for permute-and-flip. +-/ +theorem permuteAndFlipPMF_monotone + {n : CandidateCount} (q q' : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hrr : q r ≤ q' r) + (hothers : ∀ s : Fin n.succ, s ≠ r → q' s ≤ q s) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n q' ε₁ ε₂ r := by + -- First move `q` to an intermediate vector `q1` that already has the correct + -- value at coordinate `r`. + let q1 : Scores n := bumpScore q r (q' r - q r) + have hstep1 : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n q1 ε₁ ε₂ r := by + simpa [q1] using + (permuteAndFlipPMF_bumpScore_self_ge q r (q' r - q r) ε₁ ε₂) + have hothers1 : + ∀ s : Fin n.succ, s ≠ r → q' s ≤ q1 s := by + intro s hs + simp [q1, bumpScore, hs, hothers s hs] + have hstep2 : + permuteAndFlipPMF n q1 ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerOthersAlong (canonicalOrder n) q1 q' r) ε₁ ε₂ r := by + -- Then lower every non-`r` coordinate, one by one, until reaching `q'`. + -- `lowerOthersAlong` is just a proof device: it walks through the canonical + -- list of all candidates and lowers each non-`r` coordinate exactly as much + -- as needed, never touching `r`. + exact lowerOthersAlong_le + (canonicalOrder n) + (by simpa [canonicalOrder] using List.nodup_finRange n.succ) + q1 q' r ε₁ ε₂ hothers1 + have hrr1 : q1 r = q' r := by + simp [q1, bumpScore, Nat.add_sub_of_le hrr] + have hend : + lowerOthersAlong (canonicalOrder n) q1 q' r = q' := by + simpa using lowerOthersAlong_canonicalOrder_eq q1 q' r hrr1 hothers1 + calc + permuteAndFlipPMF n q ε₁ ε₂ r + ≤ permuteAndFlipPMF n q1 ε₁ ε₂ r := hstep1 + _ ≤ permuteAndFlipPMF n (lowerOthersAlong (canonicalOrder n) q1 q' r) ε₁ ε₂ r := hstep2 + _ = permuteAndFlipPMF n q' ε₁ ε₂ r := by simp [hend] + +end Global + +section PrivacyStep + +/-- +The paper's local privacy contraction for a single unit increase of `q r`. + +This is a Lean formalization of the one-step recurrence/privacy inequality used in +the supplement's proof of Theorem 1 and related recurrence statements. +-/ +theorem one_step_privacy + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + ENNReal.ofReal (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) * + permuteAndFlipPMF n (bumpScore q r 1) ε₁ ε₂ r ≤ + permuteAndFlipPMF n q ε₁ ε₂ r := by + -- We split exactly as the paper does: either `r` is already maximal, or it + -- is still below the maximum and the "easy" equality case applies. + by_cases hgap : gap q r = 0 + · exact permuteAndFlipPMF_bumpScore_self_one_of_gap_zero q r ε₁ ε₂ hgap + · have hlt : q r < maxScore q := by + refine Nat.lt_of_not_ge ?_ + intro hge + exact hgap (by simpa [gap_eq_maxScore_sub] using Nat.sub_eq_zero_of_le hge) + have hstep : q r + 1 ≤ maxScore q := Nat.succ_le_of_lt hlt + exact le_of_eq (by simpa using permuteAndFlipPMF_bumpScore_self_of_le q r 1 ε₁ ε₂ hstep) + +/-- +Iterating `one_step_privacy` yields the `k`-step contraction used in the final +range-distance theorem. +-/ +theorem bumpScore_self_privacy_pow + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) : + (ENNReal.ofReal (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)))) ^ k * + permuteAndFlipPMF n (bumpScore q r k) ε₁ ε₂ r ≤ + permuteAndFlipPMF n q ε₁ ε₂ r := by + induction k generalizing q with + | zero => + have hsame : bumpScore q r 0 = q := by + funext i + by_cases hi : i = r + · subst hi + simp [bumpScore] + · simp [bumpScore, hi] + simp [hsame] + | succ k ih => + let α : ENNReal := ENNReal.ofReal (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) + have hstep : + α * permuteAndFlipPMF n (bumpScore q r (k + 1)) ε₁ ε₂ r ≤ + permuteAndFlipPMF n (bumpScore q r k) ε₁ ε₂ r := by + -- Apply the one-step theorem to the partially bumped score vector. + -- This is the key inductive picture: compare the `k+1` vector to the + -- `k` vector, not directly to the original `q`. + simpa [α, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc, bumpScore_add] + using (one_step_privacy (q := bumpScore q r k) (r := r) (ε₁ := ε₁) (ε₂ := ε₂)) + calc + (ENNReal.ofReal (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)))) ^ (k + 1) * + permuteAndFlipPMF n (bumpScore q r (k + 1)) ε₁ ε₂ r + = α ^ k * (α * permuteAndFlipPMF n (bumpScore q r (k + 1)) ε₁ ε₂ r) := by + -- Rewrite the left-hand side so the one-step inequality can be + -- applied inside a larger multiplicative context. + simp [α, pow_succ'] + ac_rfl + _ ≤ α ^ k * permuteAndFlipPMF n (bumpScore q r k) ε₁ ε₂ r := by + exact mul_le_mul_right hstep (α ^ k) + _ ≤ permuteAndFlipPMF n q ε₁ ε₂ r := by + simpa [α] using ih (q := q) + +end PrivacyStep + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/MonotonicityLocal.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/MonotonicityLocal.lean new file mode 100644 index 00000000..c2605f7b --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/MonotonicityLocal.lean @@ -0,0 +1,462 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Paper.ClosedForm + +noncomputable section + +open scoped Classical +open PMF + +namespace SLang +namespace PermuteAndFlip +/-! +Local monotonicity lemmas for raising the selected score and lowering competing scores. + +This file contains the one-coordinate inequalities that power the global +monotonicity argument in [Monotonicity](SampCert/DifferentialPrivacy/PermuteAndFlip/Monotonicity.lean). +-/ + +/-! ### Raising the selected candidate -/ + +theorem permuteAndFlipPMF_bumpScore_self_of_le + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hmax : q r + k ≤ maxScore q) : + ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + permuteAndFlipPMF n (bumpScore q r k) ε₁ ε₂ r = + permuteAndFlipPMF n q ε₁ ε₂ r := by + have hterm (σ : Equiv.Perm (Fin n.succ)) : + ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + selectPMF ((canonicalOrder n).map σ) (bumpScore q r k) ε₁ ε₂ r) + = + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r := by + calc + ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + selectPMF ((canonicalOrder n).map σ) (bumpScore q r k) ε₁ ε₂ r) + = PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + (ENNReal.ofReal (Real.exp (- (((k * ε₁ : ℕ) : NNReal) / ε₂))) * + selectPMF ((canonicalOrder n).map σ) (bumpScore q r k) ε₁ ε₂ r) := by + ac_rfl + _ = PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + selectPMF ((canonicalOrder n).map σ) q ε₁ ε₂ r := by + -- The selector-level equality is lifted into one term of the + -- outer permutation average. + exact congrArg + (fun x => PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * x) + (selectPMF_bumpScore_self_of_le_map_canonicalOrder σ q r k ε₁ ε₂ hmax) + rw [permuteAndFlipPMF_eq_tsum_selectWeight] + rw [permuteAndFlipPMF_eq_tsum_selectWeight] + -- Summing the fixed-permutation equalities over all permutations yields the + -- full PMF statement. + rw [← ENNReal.tsum_mul_left] + refine tsum_congr (fun σ => ?_) + simpa [selectPMF_map_canonicalOrder_eq_selectWeight] using hterm σ + +theorem permuteAndFlipPMF_bumpScore_self_of_gap_zero_le + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hgap : gap q r = 0) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (bumpScore q r k) ε₁ ε₂ r := by + rw [permuteAndFlipPMF_eq_tsum_selectWeight] + rw [permuteAndFlipPMF_eq_tsum_selectWeight] + apply ENNReal.tsum_le_tsum + intro σ + exact mul_le_mul' le_rfl <| + by simpa [selectPMF_map_canonicalOrder_eq_selectWeight] using + (selectPMF_bumpScore_self_of_gap_zero_le_map_canonicalOrder σ q r k ε₁ ε₂ hgap) + +theorem permuteAndFlipPMF_lowerScore_other_of_max_eq_le + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) (hk : k ≤ q s) + (hmax : maxScore (lowerScore q s k) = maxScore q) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerScore q s k) ε₁ ε₂ r := by + rw [permuteAndFlipPMF_eq_tsum_selectWeight] + rw [permuteAndFlipPMF_eq_tsum_selectWeight] + apply ENNReal.tsum_le_tsum + intro σ + exact mul_le_mul' le_rfl <| + by simpa [selectPMF_map_canonicalOrder_eq_selectWeight] using + (selectPMF_lowerScore_other_of_max_eq_le_map_canonicalOrder σ q r s k ε₁ ε₂ hrs hk hmax) + +/-! ### Lowering a competing candidate -/ + +theorem maxScore_lowerScore_of_exists_other_argmax + {n : CandidateCount} (q : Scores n) (s : Fin n.succ) (k : ℕ) + (hk : k ≤ q s) + (hother : ∃ t : Fin n.succ, t ≠ s ∧ q t = maxScore q) : + maxScore (lowerScore q s k) = maxScore q := by + rcases hother with ⟨t, hts, htmax⟩ + refine le_antisymm ?_ ?_ + · unfold maxScore lowerScore + -- Lowering one coordinate cannot push any value above the old maximum. + refine Finset.sup_le ?_ + intro i + by_cases his : i = s + · subst his + have hqi : q i ≤ maxScore q := Finset.le_sup (s := Finset.univ) (f := q) (by simp) + simpa [lowerScore] using le_trans (Nat.sub_le (q i) k) hqi + · have hqi : q i ≤ maxScore q := Finset.le_sup (s := Finset.univ) (f := q) (by simp) + simpa [lowerScore, his] using hqi + · rw [← htmax] + unfold maxScore lowerScore + -- The witness `t` keeps the old maximum alive after lowering `s`, because + -- `t` is a different maximizing coordinate and is therefore untouched. + simpa [lowerScore, hts] using + (Finset.le_sup (s := Finset.univ) (f := fun i => q i - if i = s then k else 0) (by simp : t ∈ Finset.univ)) + +theorem permuteAndFlipPMF_lowerScore_nonunique_max_le + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) (hk : k ≤ q s) + (hother : ∃ t : Fin n.succ, t ≠ s ∧ q t = maxScore q) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerScore q s k) ε₁ ε₂ r := by + apply permuteAndFlipPMF_lowerScore_other_of_max_eq_le q r s k ε₁ ε₂ hrs hk + exact maxScore_lowerScore_of_exists_other_argmax q s k hk hother + +theorem permuteAndFlipPMF_lowerScore_unique_max_one_le + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) + (huniq : ∀ t : Fin n.succ, t ≠ s → q t < q s) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerScore q s 1) ε₁ ε₂ r := by + -- This is the delicate local monotonicity step. When `s` is the + -- unique maximizer, lowering it changes the global maximum, so we switch to + -- the paper's closed form and prove the comparison analytically there. + let ρ : ℝ := Real.exp (- ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) + have hρ0 : 0 ≤ ρ := by + dsimp [ρ] + positivity + have hρ1 : ρ ≤ 1 := by + dsimp [ρ] + have hnonneg : (0 : ℝ) ≤ ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by positivity + simpa using Real.exp_le_exp.mpr (by linarith : -(((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) ≤ 0) + have hgap' : gap (lowerScore q s 1) s = 0 := by + rw [gap_eq_maxScore_sub, maxScore_lowerScore_unique_max_one q s huniq] + simp [lowerScore] + rw [permuteAndFlipPMF_eq_ofReal_paperProb_mul_paperAlt n q ε₁ ε₂ r] + rw [permuteAndFlipPMF_eq_ofReal_paperProb_mul_paperAlt n (lowerScore q s 1) ε₁ ε₂ r] + apply ENNReal.ofReal_le_ofReal + have hprob : + paperProb q ε₁ ε₂ r = + ρ * paperProb (lowerScore q s 1) ε₁ ε₂ r := by + simpa [ρ] using paperProb_lowerScore_other_of_unique_max_one q s r ε₁ ε₂ hrs huniq + have halt : + paperAlt q r ε₁ ε₂ = + paperAltGapZeroScaled (lowerScore q s 1) r s ε₁ ε₂ ρ := by + simpa [ρ] using + paperAlt_eq_paperAltGapZeroScaled_lowerScore_unique_max_one q r s ε₁ ε₂ hrs huniq + have hscaled : + ρ * paperAltGapZeroScaled (lowerScore q s 1) r s ε₁ ε₂ ρ ≤ + paperAltGapZeroScaled (lowerScore q s 1) r s ε₁ ε₂ 1 := by + exact paperAltGapZeroScaled_mul_le_paperAltGapZero + (q := lowerScore q s 1) (r := r) (s := s) (ε₁ := ε₁) (ε₂ := ε₂) hρ0 hρ1 + have hprob_nonneg : 0 ≤ paperProb (lowerScore q s 1) ε₁ ε₂ r := by + unfold paperProb + positivity + have halt' : + paperAlt (lowerScore q s 1) r ε₁ ε₂ = + paperAltGapZeroScaled (lowerScore q s 1) r s ε₁ ε₂ 1 := by + exact paperAlt_eq_paperAltGapZeroScaled_one + (q := lowerScore q s 1) (r := r) (s := s) (ε₁ := ε₁) (ε₂ := ε₂) hrs.symm hgap' + calc + -- Rewrite both PMFs in the paper's closed form. After that, the proof is a + -- scalar inequality: one factor rescales exactly by `ρ`, and the remaining + -- reduced polynomial is monotone in the scaling parameter. + paperProb q ε₁ ε₂ r * paperAlt q r ε₁ ε₂ + = paperProb (lowerScore q s 1) ε₁ ε₂ r * + (ρ * paperAltGapZeroScaled (lowerScore q s 1) r s ε₁ ε₂ ρ) := by + rw [hprob, halt] + ring + _ ≤ paperProb (lowerScore q s 1) ε₁ ε₂ r * + paperAltGapZeroScaled (lowerScore q s 1) r s ε₁ ε₂ 1 := by + exact mul_le_mul_of_nonneg_left hscaled hprob_nonneg + _ = paperProb (lowerScore q s 1) ε₁ ε₂ r * + paperAlt (lowerScore q s 1) r ε₁ ε₂ := by + rw [halt'] + +theorem permuteAndFlipPMF_lowerScore_other_one_le + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerScore q s 1) ε₁ ε₂ r := by + by_cases hother : ∃ t : Fin n.succ, t ≠ s ∧ q t = maxScore q + · -- If `s` is not uniquely maximal, lowering it preserves the maximum score, + -- so the easy local monotonicity lemma applies. + by_cases hqs : 1 ≤ q s + · exact permuteAndFlipPMF_lowerScore_nonunique_max_le q r s 1 ε₁ ε₂ hrs hqs hother + · have hs0 : q s = 0 := by omega + have hsame : lowerScore q s 1 = q := by + funext i + by_cases his : i = s + · subst his + simp [lowerScore, hs0] + · simp [lowerScore, his] + simp [hsame] + · -- Otherwise `s` is the unique maximizer, which is exactly the analytic + -- branch handled by `permuteAndFlipPMF_lowerScore_unique_max_one_le`. + have hsmax : q s = maxScore q := by + by_cases hs : q s = maxScore q + · exact hs + · obtain ⟨t, ht⟩ := exists_argmax q + have hts : t ≠ s := by + intro hts' + apply hs + simpa [hts'] using ht + exact False.elim (hother ⟨t, hts, ht⟩) + have huniq : ∀ t : Fin n.succ, t ≠ s → q t < q s := by + intro t hts + have hle : q t ≤ maxScore q := Finset.le_sup (s := Finset.univ) (f := q) (by simp) + have hne : q t ≠ maxScore q := by + intro ht + exact hother ⟨t, hts, ht⟩ + rw [hsmax] + exact lt_of_le_of_ne hle hne + exact permuteAndFlipPMF_lowerScore_unique_max_one_le q r s ε₁ ε₂ hrs huniq + +/-! ### Iterating one-coordinate updates -/ + +theorem permuteAndFlipPMF_lowerScore_other_le + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerScore q s k) ε₁ ε₂ r := by + induction k generalizing q with + | zero => + have hsame : lowerScore q s 0 = q := by + funext i + by_cases hi : i = s + · subst hi + simp [lowerScore] + · simp [lowerScore, hi] + simp [hsame] + | succ k ih => + calc + permuteAndFlipPMF n q ε₁ ε₂ r + ≤ permuteAndFlipPMF n (lowerScore q s k) ε₁ ε₂ r := ih q + _ ≤ permuteAndFlipPMF n (lowerScore (lowerScore q s k) s 1) ε₁ ε₂ r := + -- Peel off one unit at a time so the local one-step theorem can + -- be reused uniformly. + permuteAndFlipPMF_lowerScore_other_one_le (q := lowerScore q s k) (r := r) (s := s) (ε₁ := ε₁) (ε₂ := ε₂) hrs + _ = permuteAndFlipPMF n (lowerScore q s (k + 1)) ε₁ ε₂ r := by + rw [lowerScore_add] + +theorem permuteAndFlipPMF_bumpScore_self_one_ge + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (bumpScore q r 1) ε₁ ε₂ r := by + -- Again there are two branches: if `r` is already maximal, raising it can + -- only help; otherwise we use the exact equality from the easy case and + -- discard the extra multiplicative privacy factor. + by_cases hgap : gap q r = 0 + · exact permuteAndFlipPMF_bumpScore_self_of_gap_zero_le q r 1 ε₁ ε₂ hgap + · have hlt : q r < maxScore q := by + refine Nat.lt_of_not_ge ?_ + intro hge + exact hgap (by simpa [gap_eq_maxScore_sub] using Nat.sub_eq_zero_of_le hge) + have hstep : q r + 1 ≤ maxScore q := Nat.succ_le_of_lt hlt + have heq := permuteAndFlipPMF_bumpScore_self_of_le q r 1 ε₁ ε₂ hstep + have hα1 : Real.exp (- ((((1 * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) ≤ 1 := by + have hnonneg : (0 : ℝ) ≤ ((((1 * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by positivity + simpa using Real.exp_le_exp.mpr (by linarith : -(((((1 * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) ≤ 0) + have hmul : + ENNReal.ofReal (Real.exp (- ((((1 * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ))) * + permuteAndFlipPMF n (bumpScore q r 1) ε₁ ε₂ r + ≤ permuteAndFlipPMF n (bumpScore q r 1) ε₁ ε₂ r := by + -- The privacy factor is at most `1`, so dropping it turns the exact + -- equality into the monotonicity inequality we want here. + have hαENN : + ENNReal.ofReal (Real.exp (- ((((1 * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ))) ≤ 1 := by + simpa using ENNReal.ofReal_le_ofReal hα1 + exact mul_le_of_le_one_left' hαENN + exact heq ▸ hmul + +theorem permuteAndFlipPMF_bumpScore_self_ge + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (k ε₁ : ℕ) (ε₂ : ℕ+) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (bumpScore q r k) ε₁ ε₂ r := by + induction k generalizing q with + | zero => + have hsame : bumpScore q r 0 = q := by + funext i + by_cases hi : i = r + · subst hi + simp [bumpScore] + · simp [bumpScore, hi] + simp [hsame] + | succ k ih => + calc + permuteAndFlipPMF n q ε₁ ε₂ r + ≤ permuteAndFlipPMF n (bumpScore q r k) ε₁ ε₂ r := ih q + _ ≤ permuteAndFlipPMF n (bumpScore (bumpScore q r k) r 1) ε₁ ε₂ r := + -- As in the lowering proof, iterate the one-step statement. + permuteAndFlipPMF_bumpScore_self_one_ge (q := bumpScore q r k) (r := r) (ε₁ := ε₁) (ε₂ := ε₂) + _ = permuteAndFlipPMF n (bumpScore q r (k + 1)) ε₁ ε₂ r := by + rw [bumpScore_add] + +theorem lowerOthersAlong_le + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q q' : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hothers : ∀ s : Fin n.succ, s ≠ r → q' s ≤ q s) : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerOthersAlong l q q' r) ε₁ ε₂ r := by + induction l generalizing q with + | nil => + simp [lowerOthersAlong] + | cons s l ih => + simp at hl + rcases hl with ⟨_hs_not_mem, hl⟩ + by_cases hsr : s = r + · simp [lowerOthersAlong, hsr] + exact ih hl q hothers + · have hstep : + permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n (lowerScore q s (q s - q' s)) ε₁ ε₂ r := by + -- Lower the current coordinate `s` all the way down to its target + -- value `q' s`. + exact permuteAndFlipPMF_lowerScore_other_le + (q := q) (r := r) (s := s) (k := q s - q' s) (ε₁ := ε₁) (ε₂ := ε₂) + (by intro h; exact hsr h.symm) + have hothers' : + ∀ t : Fin n.succ, t ≠ r → q' t ≤ (lowerScore q s (q s - q' s)) t := by + intro t htr + by_cases hts : t = s + · have hsle : q' t ≤ q t := hothers t htr + rw [show (lowerScore q s (q s - q' s)) t = q t - (q t - q' t) by + simp [lowerScore, hts]] + omega + · simp [lowerScore, hts] + exact hothers t htr + have htail := + ih hl (lowerScore q s (q s - q' s)) hothers' + -- Compose the one-coordinate step with the inductive hypothesis on the + -- remaining tail of the list. + simpa [lowerOthersAlong, hsr] using le_trans hstep htail + +theorem lowerOthersAlong_apply_of_not_mem + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q q' : Scores n) (r i : Fin n.succ) + (hi : i ∉ l) : + lowerOthersAlong l q q' r i = q i := by + induction l generalizing q with + | nil => + simp [lowerOthersAlong] + | cons s l ih => + simp at hl + rcases hl with ⟨_hs_not_mem, hl⟩ + have hi' : i ∉ l := by + intro hil + exact hi (by simp [hil]) + by_cases hsr : s = r + · simpa [lowerOthersAlong, hsr] using ih hl q hi' + · have his : i ≠ s := by + intro his + exact hi (by simp [his]) + simpa [lowerOthersAlong, hsr, lowerScore, his] using + (ih hl (lowerScore q s (q s - q' s)) hi') + +theorem lowerOthersAlong_apply_of_mem + {n : CandidateCount} (l : List (Fin n.succ)) (hl : l.Nodup) + (q q' : Scores n) (r i : Fin n.succ) + (hothers : ∀ s : Fin n.succ, s ≠ r → q' s ≤ q s) + (hi : i ∈ l) : + lowerOthersAlong l q q' r i = if i = r then q i else q' i := by + induction l generalizing q with + | nil => + cases hi + | cons s l ih => + simp at hl + rcases hl with ⟨hs_not_mem, hl⟩ + simp at hi + by_cases hsr : s = r + · rcases hi with rfl | hi + · have hr_not_mem : r ∉ l := by + simpa [← hsr] using hs_not_mem + have htail : + lowerOthersAlong l q q' r r = q r := by + exact lowerOthersAlong_apply_of_not_mem l hl q q' r r hr_not_mem + simpa [lowerOthersAlong, hsr] + using htail + · have hir : i ≠ r := by + intro hir + exact hs_not_mem (by simpa [hsr, hir] using hi) + simpa [lowerOthersAlong, hsr, hir] using ih hl q hothers hi + · cases hi with + | inl his => + have hsle : q' s ≤ q s := hothers s (by simpa using hsr) + have htail : + lowerOthersAlong l (lowerScore q s (q s - q' s)) q' r s = + (lowerScore q s (q s - q' s)) s := by + exact lowerOthersAlong_apply_of_not_mem l hl (lowerScore q s (q s - q' s)) q' r s hs_not_mem + calc + lowerOthersAlong (s :: l) q q' r i + = lowerOthersAlong l (lowerScore q s (q s - q' s)) q' r s := by + simp [his, lowerOthersAlong, hsr] + _ = (lowerScore q s (q s - q' s)) s := htail + _ = q' s := by + have hsub : q s - (q s - q' s) = q' s := by omega + simp [lowerScore, hsub] + _ = if i = r then q i else q' i := by + subst his + simp [hsr] + | inr hi => + have his : i ≠ s := by + intro his + exact hs_not_mem (by simpa [his] using hi) + have hothers' : + ∀ t : Fin n.succ, t ≠ r → q' t ≤ (lowerScore q s (q s - q' s)) t := by + intro t htr + by_cases hts : t = s + · have hsle : q' t ≤ q t := hothers t htr + rw [show (lowerScore q s (q s - q' s)) t = q t - (q t - q' t) by + simp [lowerScore, hts]] + omega + · simp [lowerScore, hts] + exact hothers t htr + have htail := ih hl (lowerScore q s (q s - q' s)) hothers' hi + by_cases hir : i = r + · calc + lowerOthersAlong (s :: l) q q' r i + = lowerOthersAlong l (lowerScore q s (q s - q' s)) q' r i := by + simp [lowerOthersAlong, hsr] + _ = (lowerScore q s (q s - q' s)) i := by + simpa [hir] using htail + _ = q i := by + simp [lowerScore, his] + _ = if i = r then q i else q' i := by + simp [hir] + · calc + lowerOthersAlong (s :: l) q q' r i + = lowerOthersAlong l (lowerScore q s (q s - q' s)) q' r i := by + simp [lowerOthersAlong, hsr] + _ = if i = r then (lowerScore q s (q s - q' s)) i else q' i := htail + _ = q' i := by + simp [hir] + _ = if i = r then q i else q' i := by + simp [hir] + +theorem lowerOthersAlong_canonicalOrder_eq + {n : CandidateCount} (q q' : Scores n) (r : Fin n.succ) + (hrr : q r = q' r) + (hothers : ∀ s : Fin n.succ, s ≠ r → q' s ≤ q s) : + lowerOthersAlong (canonicalOrder n) q q' r = q' := by + funext i + -- Every coordinate appears exactly once in the canonical order, so the + -- pointwise description from `lowerOthersAlong_apply_of_mem` is enough. + have hi : i ∈ canonicalOrder n := by + simp [canonicalOrder] + have hl : (canonicalOrder n).Nodup := by + simpa [canonicalOrder] using List.nodup_finRange n.succ + rw [lowerOthersAlong_apply_of_mem (canonicalOrder n) hl q q' r i hothers hi] + by_cases hir : i = r + · subst hir + simp [hrr] + · simp [hir] + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper.lean new file mode 100644 index 00000000..8e9cc766 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Paper.Polynomials +import SampCert.DifferentialPrivacy.PermuteAndFlip.Paper.Counting +import SampCert.DifferentialPrivacy.PermuteAndFlip.Paper.ClosedForm + +/-! +Reader-facing entry point for the paper-style proof ingredients. + +Reading order: +- `Paper.Polynomials` defines the real-valued paper expressions. +- `Paper.Counting` proves the permutation-counting coefficients. +- `Paper.ClosedForm` connects the executable PMF to the paper closed form. + +Key bridge theorem: +- `permuteAndFlipPMF_eq_ofReal_paperProb_mul_paperAlt` +-/ diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/ClosedForm.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/ClosedForm.lean new file mode 100644 index 00000000..8cccef46 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/ClosedForm.lean @@ -0,0 +1,395 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism.Selector + +noncomputable section + +open scoped Classical +open PMF + +namespace SLang +namespace PermuteAndFlip +/-! +PMF bridge lemmas connecting permutation averages to the paper closed form. + +Guide: +- the first block proves derivative and monotonicity facts for the paper polynomials; +- the middle block expands permutation products into subset sums; +- the final block identifies the actual PMF with the paper closed form. +-/ + +/-! ### Analytic facts about the paper polynomial -/ +theorem hasDerivAt_paperPrimitivePoly + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : + HasDerivAt + (paperPrimitivePoly q r ε₁ ε₂) + (∏ i ∈ Finset.univ.erase r, (1 - c * paperProb q ε₁ ε₂ i)) + c := by + unfold paperPrimitivePoly + have hsum : + HasDerivAt + (∑ t ∈ (Finset.univ.erase r).powerset, fun x : ℝ => + x ^ (t.card + 1) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i)) + (∑ t ∈ (Finset.univ.erase r).powerset, + c ^ t.card * (((t.card + 1 : ℝ)) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i))) + c := by + exact + (HasDerivAt.sum + (u := Finset.powerset (Finset.univ.erase r)) + (A := fun t => fun x : ℝ => + x ^ (t.card + 1) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i)) + (A' := fun t => + c ^ t.card * (((t.card + 1 : ℝ)) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i))) + (x := c) + (fun t _ht => by + have hpow : HasDerivAt (fun x : ℝ => x ^ (t.card + 1)) ((t.card + 1 : ℝ) * c ^ t.card) c := by + simpa using hasDerivAt_pow (t.card + 1) c + simpa [mul_assoc, mul_left_comm, mul_comm] using + hpow.const_mul + (((( -1 : ℝ) ^ t.card) / (t.card + 1)) * ∏ i ∈ t, paperProb q ε₁ ε₂ i))) + have hderivEq : + (∑ t ∈ (Finset.univ.erase r).powerset, + (((-1 : ℝ) ^ t.card) / (t.card + 1)) * ((t.card + 1 : ℝ) * c ^ t.card) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i) + = + ∏ i ∈ Finset.univ.erase r, (1 - c * paperProb q ε₁ ε₂ i) := by + -- This is the key algebraic step in the paper's analytic argument: + -- differentiate the alternating subset sum termwise, then recognize the + -- resulting sum as the product expansion of `∏ (1 - c * p_i)`. + calc + ∑ t ∈ (Finset.univ.erase r).powerset, + (((-1 : ℝ) ^ t.card) / (t.card + 1)) * ((t.card + 1 : ℝ) * c ^ t.card) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i + = ∑ t ∈ (Finset.univ.erase r).powerset, + (((-1 : ℝ) ^ t.card) * (c ^ t.card)) * ∏ i ∈ t, paperProb q ε₁ ε₂ i := by + apply Finset.sum_congr rfl + intro t _ht + have hne : ((t.card : ℝ) + 1) ≠ 0 := by positivity + field_simp [hne] + -- ring + _ = ∑ t ∈ (Finset.univ.erase r).powerset, + ∏ i ∈ t, (-(c * paperProb q ε₁ ε₂ i)) := by + apply Finset.sum_congr rfl + intro t _ht + have hpowneg : ((-c : ℝ) ^ t.card) = ((-1 : ℝ) ^ t.card) * c ^ t.card := by + rw [neg_eq_neg_one_mul, mul_pow] + calc + (((-1 : ℝ) ^ t.card) * (c ^ t.card)) * ∏ i ∈ t, paperProb q ε₁ ε₂ i + = ((-c : ℝ) ^ t.card) * ∏ i ∈ t, paperProb q ε₁ ε₂ i := by + rw [hpowneg] + _ = (∏ _i ∈ t, (-c : ℝ)) * ∏ i ∈ t, paperProb q ε₁ ε₂ i := by + rw [Finset.prod_const] + _ = ∏ i ∈ t, ((-c : ℝ) * paperProb q ε₁ ε₂ i) := by + rw [← Finset.prod_mul_distrib] + _ = ∏ i ∈ t, (-(c * paperProb q ε₁ ε₂ i)) := by + apply Finset.prod_congr rfl + intro i _hi + ring + _ = ∏ i ∈ Finset.univ.erase r, (1 - c * paperProb q ε₁ ε₂ i) := by + exact sum_powerset_neg_prod_eq_prod_one_sub (Finset.univ.erase r) (fun i => c * paperProb q ε₁ ε₂ i) + convert hsum using 1 + · ext x + simp [mul_assoc, mul_comm] + · simpa [mul_assoc, mul_left_comm, mul_comm] using hderivEq.symm + +theorem paperPrimitivePoly_monotoneOn_Icc + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + MonotoneOn (paperPrimitivePoly q r ε₁ ε₂) (Set.Icc (0 : ℝ) 1) := by + have hdiff : Differentiable ℝ (paperPrimitivePoly q r ε₁ ε₂) := by + intro x + exact (hasDerivAt_paperPrimitivePoly q r ε₁ ε₂ x).differentiableAt + -- The derivative is a product of terms `1 - c * p_i`, and on `c ∈ [0,1]` + -- each factor stays nonnegative because every paper probability `p_i` also + -- lies in `[0,1]`. + refine monotoneOn_of_deriv_nonneg (convex_Icc (0 : ℝ) 1) + hdiff.continuous.continuousOn hdiff.differentiableOn ?_ + intro x hx + rw [interior_Icc] at hx + rcases hx with ⟨hx0, hx1⟩ + rw [(hasDerivAt_paperPrimitivePoly q r ε₁ ε₂ x).deriv] + apply Finset.prod_nonneg + intro i _hi + have hpi0 : 0 ≤ paperProb q ε₁ ε₂ i := paperProb_nonneg q ε₁ ε₂ i + have hpi1 : paperProb q ε₁ ε₂ i ≤ 1 := paperProb_le_one q ε₁ ε₂ i + have hmul : 0 ≤ x * paperProb q ε₁ ε₂ i ∧ x * paperProb q ε₁ ε₂ i ≤ 1 := by + constructor + · exact mul_nonneg hx0.le hpi0 + · have : x ≤ 1 := hx1.le + nlinarith + linarith + +theorem paperAltScaled_mul_le_paperAlt + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) {c : ℝ} + (hc0 : 0 ≤ c) (hc1 : c ≤ 1) : + c * paperAltScaled q r ε₁ ε₂ c ≤ paperAlt q r ε₁ ε₂ := by + have hmono := paperPrimitivePoly_monotoneOn_Icc q r ε₁ ε₂ + have hc : c ∈ Set.Icc (0 : ℝ) 1 := ⟨hc0, hc1⟩ + have h1 : (1 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := by simp + have hle := hmono hc h1 hc1 + have hle' : paperPrimitiveScaled q r ε₁ ε₂ c ≤ paperPrimitiveScaled q r ε₁ ε₂ 1 := by + simpa [paperPrimitiveScaled_eq_paperPrimitivePoly] using hle + -- `paperAltScaled` is the normalized primitive divided by `c`, so the + -- monotonicity of the primitive gives exactly the scaled inequality we need. + simpa [paperPrimitiveScaled, paperAltScaled_one] using hle' + +/-! ### Expanding permutation events into subset sums -/ + +theorem beforeSet_prod_expand + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (q : Scores n) + (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + ∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i) = + ∑ t ∈ (Finset.univ.erase r).powerset, + if t ⊆ beforeSet σ r then ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) else 0 := by + calc + ∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i) + = ∑ t ∈ (beforeSet σ r).powerset, ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) := by + -- Expand the finite product by the standard powerset identity: + -- each subset chooses the `-p_i` term for exactly the indices it contains. + symm + exact sum_powerset_neg_prod_eq_prod_one_sub (beforeSet σ r) (paperProb q ε₁ ε₂) + _ = + ∑ t ∈ (Finset.univ.erase r).powerset, + if t ⊆ beforeSet σ r then ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) else 0 := by + -- Re-express the same sum over the larger ambient powerset + -- `powerset (univ.erase r)`, with an indicator telling us whether + -- the subset actually lies inside `beforeSet σ r`. + exact sum_powerset_beforeSet_eq_sum_filter σ r (fun t => ∏ i ∈ t, (-paperProb q ε₁ ε₂ i)) + +theorem sum_perm_powerset_comm + {n : CandidateCount} (r : Fin n.succ) + (f : Equiv.Perm (Fin n.succ) → Finset (Fin n.succ) → ℝ) : + ∑ σ : Equiv.Perm (Fin n.succ), ∑ t ∈ (Finset.univ.erase r).powerset, f σ t + = + ∑ t ∈ (Finset.univ.erase r).powerset, ∑ σ : Equiv.Perm (Fin n.succ), f σ t := by + classical + simpa using + (Finset.sum_comm' + (s := (Finset.univ : Finset (Equiv.Perm (Fin n.succ)))) + (t := fun _σ => (Finset.univ.erase r).powerset) + (t' := (Finset.univ.erase r).powerset) + (s' := fun _t => (Finset.univ : Finset (Equiv.Perm (Fin n.succ)))) + (f := fun σ t => f σ t) + (by + intro σ t + simp)) + +theorem sum_beforeSet_prod_eq_sum_neg_prod_coeff + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + ∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + ∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i) + = + ∑ t ∈ (Finset.univ.erase r).powerset, + (((t.card + 1 : ℕ) : ℝ)⁻¹) * ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) := by + let P : Finset (Finset (Fin n.succ)) := (Finset.univ.erase r).powerset + let G : Finset (Fin n.succ) → ℝ := fun t => ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) + calc + ∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + ∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i) + = + ∑ σ : Equiv.Perm (Fin n.succ), + ∑ t ∈ P, + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then G t else 0) := by + apply Finset.sum_congr rfl + intro σ _hσ + simp [P, G, beforeSet_prod_expand σ q r ε₁ ε₂, Finset.mul_sum] + _ = + ∑ t ∈ P, + ∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then G t else 0) := by + -- Swap the order of summation: first choose the subset `t`, + -- then count how often it appears before `r` under a uniform permutation. + simpa [P] using + (sum_perm_powerset_comm r + (fun σ t => + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then G t else 0))) + _ = + ∑ t ∈ P, + (∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then 1 else 0)) * G t := by + -- Now factor out the subset-dependent term `G t`; the inner sum + -- is exactly the coefficient "probability that all of `t` occur before `r`". + apply Finset.sum_congr rfl + intro t _ht + have hfactor : + ∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then G t else 0) + = + ∑ σ : Equiv.Perm (Fin n.succ), + ((PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then 1 else 0)) * G t := by + apply Finset.sum_congr rfl + intro σ _hσ + split <;> ring + rw [hfactor, Finset.sum_mul] + _ = + ∑ t ∈ P, (((t.card + 1 : ℕ) : ℝ)⁻¹) * G t := by + apply Finset.sum_congr rfl + intro t ht + have ht' : t ⊆ Finset.univ.erase r := by + simpa [P] using (Finset.mem_powerset.mp ht) + have hr' : r ∉ t := by + intro h + exact (Finset.mem_erase.mp (ht' (by simp [h]))).1 rfl + rw [real_subset_beforeSet_coeff (r := r) (t := t) hr'] + _ = ∑ t ∈ (Finset.univ.erase r).powerset, + (((t.card + 1 : ℕ) : ℝ)⁻¹) * ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) := by + rfl + +theorem tsum_beforeSet_prod_eq_ofReal_paperAlt + (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + ∑' σ : Equiv.Perm (Fin n.succ), + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + ∏ i ∈ beforeSet σ r, exactCoinPMF (gap q i * ε₁) ε₂ false + = ENNReal.ofReal (paperAlt q r ε₁ ε₂) := by + rw [tsum_fintype] + calc + ∑ σ : Equiv.Perm (Fin n.succ), + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + ∏ i ∈ beforeSet σ r, exactCoinPMF (gap q i * ε₁) ε₂ false + = + ∑ σ : Equiv.Perm (Fin n.succ), + ENNReal.ofReal + ((PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + ∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i)) := by + apply Finset.sum_congr rfl + intro σ _hσ + have hprod : + ∏ i ∈ beforeSet σ r, exactCoinPMF (gap q i * ε₁) ε₂ false = + ENNReal.ofReal (∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i)) := by + calc + ∏ i ∈ beforeSet σ r, exactCoinPMF (gap q i * ε₁) ε₂ false + = ∏ i ∈ beforeSet σ r, ENNReal.ofReal (1 - paperProb q ε₁ ε₂ i) := by + apply Finset.prod_congr rfl + intro i _hi + exact (ofReal_one_sub_paperProb_eq_exactCoin_false q ε₁ ε₂ i).symm + _ = ENNReal.ofReal (∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i)) := by + symm + apply ENNReal.ofReal_prod_of_nonneg + intro i _hi + have hle := paperProb_le_one q ε₁ ε₂ i + exact sub_nonneg.mpr hle + calc + PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ * + ∏ i ∈ beforeSet σ r, exactCoinPMF (gap q i * ε₁) ε₂ false + = ENNReal.ofReal ((PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal) * + ENNReal.ofReal (∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i)) := by + rw [ENNReal.ofReal_toReal] + · rw [hprod] + · simp + _ = + ENNReal.ofReal + ((PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + ∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i)) := by + rw [← ENNReal.ofReal_mul] + exact ENNReal.toReal_nonneg + _ = + ENNReal.ofReal + (∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + ∏ i ∈ beforeSet σ r, (1 - paperProb q ε₁ ε₂ i)) := by + -- Convert the finite ENNReal average into an ordinary real-valued + -- sum, where the counting lemmas can be applied directly. + symm + apply ENNReal.ofReal_sum_of_nonneg + intro σ _hσ + apply mul_nonneg + · exact ENNReal.toReal_nonneg + · exact Finset.prod_nonneg (fun i _hi => by + have hle := paperProb_le_one q ε₁ ε₂ i + exact sub_nonneg.mpr hle) + _ = ENNReal.ofReal (paperAlt q r ε₁ ε₂) := by + -- The remaining step is a direct substitution: the finite + -- real-valued sum is exactly the coefficient formula proved earlier, + -- and that formula is how `paperAlt` was defined. + rw [sum_beforeSet_prod_eq_sum_neg_prod_coeff, paperAlt_eq_sum_neg_prod] + +/-- +This is the main closed-form bridge to the paper: the PMF of output `r` +matches the paper's real-valued expression `paperProb * paperAlt`. + +It packages the supplement's closed-form derivation used in the +proof of Theorem 1. +-/ +theorem permuteAndFlipPMF_eq_exactCoin_mul_ofReal_paperAlt + (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + permuteAndFlipPMF n q ε₁ ε₂ r = + exactCoinPMF (gap q r * ε₁) ε₂ true * ENNReal.ofReal (paperAlt q r ε₁ ε₂) := by + rw [permuteAndFlipPMF_eq_coin_mul_tsum_beforeSet_prod] + rw [tsum_beforeSet_prod_eq_ofReal_paperAlt] + +theorem permuteAndFlipPMF_eq_ofReal_paperProb_mul_paperAlt + (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) : + permuteAndFlipPMF n q ε₁ ε₂ r = + ENNReal.ofReal (paperProb q ε₁ ε₂ r * paperAlt q r ε₁ ε₂) := by + rw [permuteAndFlipPMF_eq_exactCoin_mul_ofReal_paperAlt] + rw [exactCoinPMF_apply_true, paperProb] + rw [← ENNReal.ofReal_mul] + · positivity + +theorem permuteAndFlipPMF_max_eq_ofReal_paperAlt + (n : CandidateCount) (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (r : Fin n.succ) + (hgap : gap q r = 0) : + permuteAndFlipPMF n q ε₁ ε₂ r = ENNReal.ofReal (paperAlt q r ε₁ ε₂) := by + rw [permuteAndFlipPMF_eq_exactCoin_mul_ofReal_paperAlt] + simp [hgap] + +theorem permuteAndFlipPMF_bumpScore_self_one_of_gap_zero_eq_ofReal_paperAltScaled + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hgap : gap q r = 0) : + permuteAndFlipPMF n (bumpScore q r 1) ε₁ ε₂ r = + ENNReal.ofReal + (paperAltScaled q r ε₁ ε₂ (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)))) := by + have hgap' : gap (bumpScore q r 1) r = 0 := by + have hmax : maxScore q ≤ q r + 1 := by + rw [maxScore_eq_of_gap_zero q r hgap] + omega + simpa using gap_bumpScore_self_of_ge q r 1 hmax + rw [permuteAndFlipPMF_max_eq_ofReal_paperAlt n (bumpScore q r 1) ε₁ ε₂ r hgap'] + rw [paperAlt_bumpScore_self_one_of_gap_zero q r ε₁ ε₂ hgap] + +theorem permuteAndFlipPMF_bumpScore_self_one_of_gap_zero + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hgap : gap q r = 0) : + ENNReal.ofReal (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) * + permuteAndFlipPMF n (bumpScore q r 1) ε₁ ε₂ r ≤ + permuteAndFlipPMF n q ε₁ ε₂ r := by + -- Once `r` is already maximal, both PMFs can be rewritten entirely in the + -- paper's closed form, and the inequality reduces to the scalar monotonicity + -- statement `paperAltScaled_mul_le_paperAlt`. + rw [permuteAndFlipPMF_bumpScore_self_one_of_gap_zero_eq_ofReal_paperAltScaled q r ε₁ ε₂ hgap] + rw [permuteAndFlipPMF_max_eq_ofReal_paperAlt n q ε₁ ε₂ r hgap] + rw [← ENNReal.ofReal_mul] + · apply ENNReal.ofReal_le_ofReal + have hρ0 : 0 ≤ Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) := by + positivity + have hρ1 : Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) ≤ 1 := by + have hnonneg : (0 : ℝ) ≤ (((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) := by positivity + have hle0 : -((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) ≤ 0 := by + linarith + have hle : Real.exp (-((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) ≤ Real.exp 0 := by + exact Real.exp_le_exp.mpr hle0 + convert hle using 1 + simp + exact paperAltScaled_mul_le_paperAlt q r ε₁ ε₂ hρ0 hρ1 + · positivity + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/Counting.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/Counting.lean new file mode 100644 index 00000000..8bd3fcf1 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/Counting.lean @@ -0,0 +1,680 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Paper.Polynomials + +noncomputable section + +open scoped Classical +open PMF + +namespace SLang +namespace PermuteAndFlip +/-! +Counting and permutation-combinatorics lemmas for the paper-style proof. + +Reading guide: +- `latestIn` and `beforeSet` encode the paper's "items before `r` in a permutation" events; +- the middle of the file proves the exact uniform coefficient `1 / (|t| + 1)`; +- the later lemmas package those coefficients for the closed-form PMF bridge. +-/ + +/-! ### Part I: latest-in combinatorics + +This first block proves a symmetry fact about uniform random permutations: +for a fixed nonempty finite set `s`, every element of `s` is equally likely to +be the latest element of `s` in the permutation. + +The paper uses this symmetry implicitly to obtain the coefficient +`1 / (|t| + 1)` that appears in the closed-form PMF. +-/ + +def latestIn {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (s : Finset (Fin n.succ)) (r : Fin n.succ) : Prop := + r ∈ s ∧ ∀ i ∈ s, σ.symm i ≤ σ.symm r + +@[simp] +theorem swap_trans_symm_apply {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (r t i : Fin n.succ) : + (σ.trans (Equiv.swap r t)).symm i = σ.symm ((Equiv.swap r t) i) := by + simp [Equiv.symm_trans_apply] + +theorem latestIn_unique {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (s : Finset (Fin n.succ)) + {r t : Fin n.succ} (hr : latestIn σ s r) (ht : latestIn σ s t) : + r = t := by + rcases hr with ⟨hrmem, hrlt⟩ + rcases ht with ⟨htmem, htlt⟩ + apply σ.symm.injective + exact le_antisymm (htlt r hrmem) (hrlt t htmem) + +theorem exists_latestIn {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (s : Finset (Fin n.succ)) (hs : s.Nonempty) : + ∃ r, latestIn σ s r := by + obtain ⟨r, hrmem, hrmax⟩ := Finset.exists_max_image s σ.symm hs + refine ⟨r, hrmem, ?_⟩ + intro i hi + exact hrmax i hi + +theorem existsUnique_latestIn {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (s : Finset (Fin n.succ)) (hs : s.Nonempty) : + ∃! r, latestIn σ s r := by + obtain ⟨r, hr⟩ := exists_latestIn σ s hs + refine ⟨r, hr, ?_⟩ + intro t ht + exact latestIn_unique σ s ht hr + +theorem latestIn_swap {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (s : Finset (Fin n.succ)) + (r t : Fin n.succ) (hr : r ∈ s) (ht : t ∈ s) : + latestIn σ s r → latestIn (σ.trans (Equiv.swap r t)) s t := by + by_cases hrt : r = t + · subst hrt + simp [latestIn] + · intro h + rcases h with ⟨_, hlt⟩ + refine ⟨ht, ?_⟩ + intro i hi + have hmem : (Equiv.swap r t) i ∈ s := by + by_cases hir : i = r + · subst hir + simpa [Equiv.swap_apply_def, hrt] using ht + · by_cases hit : i = t + · subst hit + simpa [Equiv.swap_apply_def, hrt] using hr + · simpa [Equiv.swap_apply_def, hir, hit] using hi + have hbound : σ.symm ((Equiv.swap r t) i) ≤ σ.symm ((Equiv.swap r t) t) := by + simpa [Equiv.swap_apply_def, hrt] using hlt ((Equiv.swap r t) i) hmem + simpa [swap_trans_symm_apply, Equiv.swap_apply_def, hrt] using hbound + +theorem latestIn_swap_iff {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (s : Finset (Fin n.succ)) + (r t : Fin n.succ) (hr : r ∈ s) (ht : t ∈ s) : + latestIn σ s r ↔ latestIn (σ.trans (Equiv.swap r t)) s t := by + constructor + · exact latestIn_swap σ s r t hr ht + · intro h + have h' : + latestIn ((σ.trans (Equiv.swap r t)).trans (Equiv.swap t r)) s r := + latestIn_swap (σ.trans (Equiv.swap r t)) s t r ht hr h + have hcomp : (σ.trans (Equiv.swap r t)).trans (Equiv.swap t r) = σ := by + ext x + by_cases hsxr : σ x = r + · by_cases hsxt : σ x = t + · have : r = t := hsxr.symm.trans hsxt + subst this + simp [hsxr] + · simp [Equiv.trans_apply, hsxr] + · by_cases hsxt : σ x = t + · simp [Equiv.trans_apply, hsxt] + · simp [Equiv.trans_apply, Equiv.swap_apply_def, hsxr, hsxt] + simpa [hcomp] using h' + +theorem card_filter_latestIn_eq {n : CandidateCount} + (s : Finset (Fin n.succ)) (_hs : s.Nonempty) + {r t : Fin n.succ} (hr : r ∈ s) (ht : t ∈ s) : + (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s r).card = + (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s t).card := by + classical + refine Finset.card_nbij' + (fun σ => σ.trans (Equiv.swap r t)) + (fun σ => σ.trans (Equiv.swap t r)) + ?_ ?_ ?_ ?_ + · intro σ hσ + simpa [Finset.mem_filter] using + (latestIn_swap_iff σ s r t hr ht).mp (by simpa [Finset.mem_filter] using hσ) + · intro σ hσ + simpa [Finset.mem_filter] using + (latestIn_swap_iff σ s t r ht hr).mp (by simpa [Finset.mem_filter] using hσ) + · intro σ _hσ + ext x + simp [Equiv.trans_apply] + by_cases hsxr : σ x = r + · by_cases hsxt : σ x = t + · have : r = t := hsxr.symm.trans hsxt + subst this + simp [hsxr] + · simp [hsxr] + · by_cases hsxt : σ x = t + · simp [hsxt] + · simp [Equiv.swap_apply_def, hsxr, hsxt] + · intro σ _hσ + ext x + simp [Equiv.trans_apply] + by_cases hsxt : σ x = t + · by_cases hsxr : σ x = r + · have : t = r := hsxt.symm.trans hsxr + subst this + simp [hsxt] + · simp [hsxt] + · by_cases hsxr : σ x = r + · simp [hsxr] + · simp [Equiv.swap_apply_def, hsxr, hsxt] + +def latestChoice {n : CandidateCount} + (s : Finset (Fin n.succ)) (hs : s.Nonempty) (σ : Equiv.Perm (Fin n.succ)) : Fin n.succ := + Classical.choose (existsUnique_latestIn σ s hs).exists + +theorem latestChoice_spec {n : CandidateCount} + (s : Finset (Fin n.succ)) (hs : s.Nonempty) (σ : Equiv.Perm (Fin n.succ)) : + latestIn σ s (latestChoice s hs σ) := by + exact (Classical.choose_spec (existsUnique_latestIn σ s hs).exists) + +theorem latestChoice_mem {n : CandidateCount} + (s : Finset (Fin n.succ)) (hs : s.Nonempty) (σ : Equiv.Perm (Fin n.succ)) : + latestChoice s hs σ ∈ s := by + exact (latestChoice_spec s hs σ).1 + +theorem latestChoice_eq_iff {n : CandidateCount} + (s : Finset (Fin n.succ)) (hs : s.Nonempty) (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) : + latestChoice s hs σ = r ↔ latestIn σ s r := by + constructor + · intro h + subst h + exact latestChoice_spec s hs σ + · intro hr + exact latestIn_unique σ s (latestChoice_spec s hs σ) hr + +theorem sum_card_filter_latestIn + {n : CandidateCount} (s : Finset (Fin n.succ)) (hs : s.Nonempty) : + Finset.sum s (fun r => (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s r).card) = + Fintype.card (Equiv.Perm (Fin n.succ)) := by + classical + calc + Finset.sum s (fun r => (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s r).card) + = Finset.sum s (fun r => (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestChoice s hs σ = r).card) := by + apply Finset.sum_congr rfl + intro r _hr + congr + ext σ + simp [latestChoice_eq_iff] + _ = (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestChoice s hs σ ∈ s).card := by + exact Finset.sum_card_fiberwise_eq_card_filter Finset.univ s (latestChoice s hs) + _ = Fintype.card (Equiv.Perm (Fin n.succ)) := by + simp [latestChoice_mem] + +theorem card_filter_latestIn_eq_card_div + {n : CandidateCount} (s : Finset (Fin n.succ)) (hs : s.Nonempty) (r : Fin n.succ) (hr : r ∈ s) : + s.card * (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s r).card = + Fintype.card (Equiv.Perm (Fin n.succ)) := by + have hconst : + ∀ t ∈ s, + (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s t).card = + (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s r).card := by + intro t ht + symm + exact card_filter_latestIn_eq s hs hr ht + calc + s.card * (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s r).card + = Finset.sum s (fun t => (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ s t).card) := by + exact (Finset.sum_const_nat hconst).symm + _ = Fintype.card (Equiv.Perm (Fin n.succ)) := by + exact sum_card_filter_latestIn s hs + +/-! ### Part II: subset events and coefficients + +This second block turns the latest-in symmetry into the exact probability of +the event `t ⊆ beforeSet σ r`, and then packages that coefficient for the PMF +bridge in `Paper.ClosedForm`. +-/ + +theorem latestIn_insert_iff {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) (t : Finset (Fin n.succ)) + (hr : r ∉ t) : + latestIn σ (insert r t) r ↔ ∀ i ∈ t, σ.symm i < σ.symm r := by + constructor + · intro h i hi + rcases h with ⟨_, hle⟩ + have hne : i ≠ r := by + intro hir + exact hr (hir ▸ hi) + have hle' : σ.symm i ≤ σ.symm r := hle i (by simp [hi]) + exact lt_of_le_of_ne hle' (by + intro heq + apply hne + exact σ.symm.injective heq) + · intro h + refine ⟨by simp, ?_⟩ + intro i hi + rcases Finset.mem_insert.mp hi with rfl | hi' + · exact le_rfl + · exact (h i hi').le + +def latestInCount {n : CandidateCount} (r : Fin n.succ) (t : Finset (Fin n.succ)) : ℕ := + (Finset.univ.filter fun σ : Equiv.Perm (Fin n.succ) => latestIn σ (insert r t) r).card + +/-- Uniform mass assigned to the event that `r` is latest in `insert r t`. -/ +def latestInMass {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) (t : Finset (Fin n.succ)) : ENNReal := + ((PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) : PMF (Equiv.Perm (Fin n.succ))) σ) * + (latestInCount r t : ENNReal) + +def beforeSet {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) : Finset (Fin n.succ) := + (Finset.univ.erase r).filter fun i => σ.symm i < σ.symm r + +theorem latestInMass_eq_inv_card_insert + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) (t : Finset (Fin n.succ)) + (_hr : r ∉ t) : + latestInMass σ r t = (((insert r t).card : ENNReal)⁻¹) := by + classical + have hs : (insert r t).Nonempty := by simp + have hcount : + (insert r t).card * latestInCount r t = Fintype.card (Equiv.Perm (Fin n.succ)) := by + simpa [latestInCount] using card_filter_latestIn_eq_card_div (insert r t) hs r (by simp) + have hcard_ne : ((insert r t).card : ENNReal) ≠ 0 := by + exact_mod_cast (Finset.card_ne_zero.mpr hs) + have htot_ne : (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal) ≠ 0 := by + exact_mod_cast (Fintype.card_ne_zero : Fintype.card (Equiv.Perm (Fin n.succ)) ≠ 0) + have hcount_cast : + ((insert r t).card : ENNReal) * (latestInCount r t : ENNReal) = + (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal) := by + exact_mod_cast hcount + have hcount' : ((latestInCount r t : ℕ) : ENNReal) = ((insert r t).card : ENNReal)⁻¹ * + (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal) := by + calc + ((latestInCount r t : ℕ) : ENNReal) + = ((insert r t).card : ENNReal)⁻¹ * (((insert r t).card : ENNReal) * (latestInCount r t : ENNReal)) := by + rw [← mul_assoc, ENNReal.inv_mul_cancel hcard_ne (by simp), one_mul] + _ = ((insert r t).card : ENNReal)⁻¹ * + (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal) := by + rw [hcount_cast] + calc + latestInMass σ r t + = (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal)⁻¹ * (latestInCount r t : ENNReal) := by + simp [latestInMass, latestInCount, PMF.uniformOfFintype_apply] + _ = (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal)⁻¹ * + (((insert r t).card : ENNReal)⁻¹ * + (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal)) := by + rw [hcount'] + _ = ((insert r t).card : ENNReal)⁻¹ := by + calc + (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal)⁻¹ * + (((insert r t).card : ENNReal)⁻¹ * + (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal)) + = ((insert r t).card : ENNReal)⁻¹ * + ((Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal)⁻¹ * + (Fintype.card (Equiv.Perm (Fin n.succ)) : ENNReal)) := by + ac_rfl + _ = ((insert r t).card : ENNReal)⁻¹ * 1 := by + rw [ENNReal.inv_mul_cancel htot_ne (by simp)] + _ = ((insert r t).card : ENNReal)⁻¹ := by rw [mul_one] + +theorem subset_beforeSet_iff_latestIn_insert + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) (t : Finset (Fin n.succ)) + (hr : r ∉ t) : + t ⊆ beforeSet σ r ↔ latestIn σ (insert r t) r := by + constructor + · intro hsub + rw [latestIn_insert_iff σ r t hr] + intro i hi + have hi' : i ∈ beforeSet σ r := hsub hi + simp [beforeSet] at hi' + exact hi'.2 + · intro h + rw [latestIn_insert_iff σ r t hr] at h + intro i hi + have hir : i ≠ r := by + intro hir + exact hr (hir ▸ hi) + simp [beforeSet, hir, h i hi] + +theorem latestInMass_eq_inv_card_succ + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) (t : Finset (Fin n.succ)) + (hr : r ∉ t) : + latestInMass σ r t = ((t.card + 1 : ℕ) : ENNReal)⁻¹ := by + rw [latestInMass_eq_inv_card_insert σ r t hr] + rw [Finset.card_insert_of_notMem hr] + +theorem indexOf_map_canonicalOrder + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) : + (((List.finRange n.succ).map σ).idxOf r) = (σ.symm r).1 := by + have hnodup : (((List.finRange n.succ).map σ)).Nodup := by + simpa using (List.nodup_finRange n.succ).map σ.injective + have hlen : (σ.symm r).1 < (((List.finRange n.succ).map σ)).length := by + simpa using (σ.symm r).2 + simpa [List.getElem_map, hlen] using hnodup.idxOf_getElem (σ.symm r).1 hlen + +theorem take_ofFn_eq_ofFn_prefix + {α : Type} {n : ℕ} (f : Fin n → α) (k : Fin n) : + (List.ofFn f).take k = List.ofFn (fun j : Fin k => f ⟨j, Nat.lt_trans j.2 k.2⟩) := by + apply List.ext_getElem + · simp + · intro i hi₁ hi₂ + have hk : (i : ℕ) < (k : ℕ) := by + simpa [List.length_ofFn] using hi₁ + have hi_len : (i : ℕ) < (List.ofFn f).length := by + simpa [List.length_ofFn] using Nat.lt_trans hi₂ (by simp [List.length_ofFn]) + calc + ((List.ofFn f).take k)[i] + = (List.ofFn f)[i] := by + exact List.getElem_take (h := hi₁) + _ = f ⟨i, by simpa [List.length_ofFn] using hi_len⟩ := by + simp [List.getElem_ofFn] + _ = (List.ofFn fun j : Fin k => f ⟨j, Nat.lt_trans j.2 k.2⟩)[i] := by + simp [List.getElem_ofFn] + +def beforeEmbedding {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) : Fin (σ.symm r) ↪ Fin n.succ where + toFun j := σ ⟨j, Nat.lt_trans j.2 (σ.symm r).2⟩ + inj' := by + intro a b hab + apply Fin.ext + simpa using congrArg Fin.val (σ.injective hab) + +theorem beforeSet_eq_map_beforeEmbedding + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) : + beforeSet σ r = Finset.univ.map (beforeEmbedding σ r) := by + classical + ext i + constructor + · intro hi + rcases Finset.mem_filter.mp hi with ⟨_hi_univ, hi_lt⟩ + refine Finset.mem_map.mpr ?_ + refine ⟨⟨(σ.symm i).1, hi_lt⟩, ?_, ?_⟩ + · simp + · simp [beforeEmbedding] + · intro hi + rcases Finset.mem_map.mp hi with ⟨j, _hj, hji⟩ + have hsymm : σ.symm i = ⟨(j : ℕ), Nat.lt_trans j.2 (σ.symm r).2⟩ := by + apply σ.injective + simpa [beforeEmbedding] using hji.symm + refine Finset.mem_filter.mpr ?_ + refine ⟨?_, ?_⟩ + · refine Finset.mem_erase.mpr ?_ + constructor + · intro hir + have hlt : σ.symm i < σ.symm r := by + rw [hsymm] + exact j.2 + have : σ.symm r < σ.symm r := by + have : False := by + simp [hir] at hlt + exact False.elim this + exact lt_irrefl _ this + · simp + · rw [hsymm] + exact j.2 + +theorem prefix_prod_eq_beforeSet_prod + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) + (g : Fin n.succ → ENNReal) : + (((List.ofFn σ).take (σ.symm r)).map g).prod = ∏ i ∈ beforeSet σ r, g i := by + rw [take_ofFn_eq_ofFn_prefix σ (σ.symm r), List.map_ofFn, List.prod_ofFn] + rw [beforeSet_eq_map_beforeEmbedding σ r] + rw [Finset.prod_map] + rfl + +/-! ### Part III: coefficients specialized to the paper probabilities -/ + +@[simp] +theorem ofReal_one_sub_paperProb_eq_exactCoin_false {n : CandidateCount} + (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (i : Fin n.succ) : + ENNReal.ofReal (1 - paperProb q ε₁ ε₂ i) = exactCoinPMF (gap q i * ε₁) ε₂ false := by + rw [exactCoinPMF_apply_false, paperProb] + have hnonneg : + 0 ≤ Real.exp (- ((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) := by + positivity + simpa using (ENNReal.ofReal_sub (1 : ℝ) hnonneg) + +theorem paperProb_nonneg {n : CandidateCount} + (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (i : Fin n.succ) : + 0 ≤ paperProb q ε₁ ε₂ i := by + unfold paperProb + positivity + +theorem paperProb_le_one {n : CandidateCount} + (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (i : Fin n.succ) : + paperProb q ε₁ ε₂ i ≤ 1 := by + unfold paperProb + have hnonneg : 0 ≤ ((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by positivity + have hle : Real.exp (- ((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) ≤ Real.exp 0 := by + exact Real.exp_le_exp.mpr (by linarith) + simpa using hle + +theorem beforeSet_subset_erase {n : CandidateCount} + (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) : + beforeSet σ r ⊆ Finset.univ.erase r := by + intro i hi + exact (Finset.mem_filter.mp hi).1 + +theorem powerset_beforeSet_eq_filter + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) : + (beforeSet σ r).powerset = + ((Finset.univ.erase r).powerset).filter (fun t => t ⊆ beforeSet σ r) := by + ext t + constructor + · intro ht + simp [Finset.mem_powerset] at ht ⊢ + exact ⟨Set.Subset.trans ht (beforeSet_subset_erase σ r), ht⟩ + · intro ht + simp [Finset.mem_powerset] at ht ⊢ + exact ht.2 + +theorem sum_powerset_beforeSet_eq_sum_filter + {n : CandidateCount} (σ : Equiv.Perm (Fin n.succ)) (r : Fin n.succ) + (F : Finset (Fin n.succ) → ℝ) : + ∑ t ∈ (beforeSet σ r).powerset, F t = + ∑ t ∈ (Finset.univ.erase r).powerset, if t ⊆ beforeSet σ r then F t else 0 := by + rw [powerset_beforeSet_eq_filter σ r, Finset.sum_filter] + +theorem real_subset_beforeSet_coeff + {n : CandidateCount} (r : Fin n.succ) (t : Finset (Fin n.succ)) + (hr : r ∉ t) : + ∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then 1 else 0) + = ((t.card + 1 : ℕ) : ℝ)⁻¹ := by + let u : ℝ := (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) (Equiv.refl (Fin n.succ))).toReal + have hu : ∀ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal = u := by + intro σ + simp [u, PMF.uniformOfFintype_apply] + calc + ∑ σ : Equiv.Perm (Fin n.succ), + (PMF.uniformOfFintype (Equiv.Perm (Fin n.succ)) σ).toReal * + (if t ⊆ beforeSet σ r then 1 else 0) + = u * ∑ σ : Equiv.Perm (Fin n.succ), (if t ⊆ beforeSet σ r then 1 else 0) := by + -- Under the uniform distribution on permutations, every permutation + -- has the same mass `u`, so only the event count matters. + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro σ _hσ + rw [hu σ] + _ = u * latestInCount r t := by + -- The event "`t` appears before `r`" is the same as "`r` is latest in `insert r t`". + simp [latestInCount, subset_beforeSet_iff_latestIn_insert, hr] + _ = ((t.card + 1 : ℕ) : ℝ)⁻¹ := by + -- `latestInMass_eq_inv_card_succ` is exactly the equal-share counting + -- statement: among the `t.card + 1` elements of `insert r t`, each is + -- equally likely to be the latest one. + have hmass := + congrArg ENNReal.toReal + (latestInMass_eq_inv_card_succ (σ := Equiv.refl (Fin n.succ)) r t hr) + have htoRealInv : ((((t.card + 1 : ℕ) : ENNReal)⁻¹).toReal) = ((t.card + 1 : ℕ) : ℝ)⁻¹ := by + rw [ENNReal.toReal_inv] + rw [ENNReal.toReal_natCast] + rw [htoRealInv] at hmass + simpa [u, latestInMass, PMF.uniformOfFintype_apply] using hmass + +theorem prod_neg_paperProb + {n : CandidateCount} (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (t : Finset (Fin n.succ)) : + ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) = + ((-1 : ℝ) ^ t.card) * ∏ i ∈ t, paperProb q ε₁ ε₂ i := by + calc + ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) + = ∏ i ∈ t, ((-1 : ℝ) * paperProb q ε₁ ε₂ i) := by + apply Finset.prod_congr rfl + intro i _hi + ring + _ = (∏ _i ∈ t, (-1 : ℝ)) * ∏ i ∈ t, paperProb q ε₁ ε₂ i := by + rw [Finset.prod_mul_distrib] + _ = ((-1 : ℝ) ^ t.card) * ∏ i ∈ t, paperProb q ε₁ ε₂ i := by + rw [Finset.prod_const] + +theorem paperAlt_eq_sum_neg_prod + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + paperAlt q r ε₁ ε₂ = + ∑ t ∈ (Finset.univ.erase r).powerset, + (((t.card + 1 : ℕ) : ℝ)⁻¹) * ∏ i ∈ t, (-paperProb q ε₁ ε₂ i) := by + unfold paperAlt + apply Finset.sum_congr rfl + intro t _ht + rw [prod_neg_paperProb q ε₁ ε₂ t] + have hne : ((t.card : ℝ) + 1) ≠ 0 := by positivity + field_simp [hne] + rw [Nat.cast_add, Nat.cast_one, mul_add, mul_one] + ring + +theorem paperProb_bumpScore_other_of_gap_zero + {n : CandidateCount} (q : Scores n) (r i : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hir : i ≠ r) (hgap : gap q r = 0) : + paperProb (bumpScore q r 1) ε₁ ε₂ i = + Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) * paperProb q ε₁ ε₂ i := by + unfold paperProb + rw [gap_bumpScore_other_of_gap_zero q r i 1 hir hgap] + rw [Nat.add_mul, one_mul] + have hdiv : + ((((gap q i * ε₁ + ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) = + ((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) + + ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by + have hden : (((ε₂ : NNReal) : ℝ)) ≠ 0 := by positivity + have hnum : ((gap q i * ε₁ + ε₁ : ℕ) : NNReal) = + ((gap q i * ε₁ : ℕ) : NNReal) + ((ε₁ : ℕ) : NNReal) := by + exact_mod_cast (show gap q i * ε₁ + ε₁ = gap q i * ε₁ + ε₁ by rfl) + rw [hnum, NNReal.coe_div, NNReal.coe_div] + simp [add_div] + have hdiv' : + - ((((gap q i * ε₁ + ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) = + - ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) + + - ((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by + linarith + change + Real.exp (- ((((gap q i * ε₁ + ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) = + Real.exp (- ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) * + Real.exp (- ((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) + rw [hdiv', Real.exp_add] + +theorem paperAlt_bumpScore_self_one_of_gap_zero + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hgap : gap q r = 0) : + paperAlt (bumpScore q r 1) r ε₁ ε₂ = + paperAltScaled q r ε₁ ε₂ (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) := by + unfold paperAlt paperAltScaled + apply Finset.sum_congr rfl + intro t ht + have ht' : t ⊆ Finset.univ.erase r := by + simpa using (Finset.mem_powerset.mp ht) + have hrnot : r ∉ t := by + exact fun hrmem => (Finset.mem_erase.mp (ht' hrmem)).1 rfl + calc + (((-1 : ℝ) ^ t.card) / (t.card + 1)) * ∏ i ∈ t, paperProb (bumpScore q r 1) ε₁ ε₂ i + = (((-1 : ℝ) ^ t.card) / (t.card + 1)) * + ∏ i ∈ t, (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) * paperProb q ε₁ ε₂ i) := by + congr 1 + apply Finset.prod_congr rfl + intro i hi + apply paperProb_bumpScore_other_of_gap_zero + intro hir + exact hrnot (hir ▸ hi) + exact hgap + _ = (((-1 : ℝ) ^ t.card) / (t.card + 1)) * + ((∏ _i ∈ t, Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i) := by + rw [Finset.prod_mul_distrib] + _ = (((-1 : ℝ) ^ t.card) / (t.card + 1)) * + (((Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) ^ t.card) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i) := by + rw [Finset.prod_const] + _ = (((-1 : ℝ) ^ t.card) / (t.card + 1)) * + (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) ^ t.card) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i := by + ring + +theorem paperProb_lowerScore_other_of_unique_max_one + {n : CandidateCount} (q : Scores n) (s i : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (his : i ≠ s) (huniq : ∀ t : Fin n.succ, t ≠ s → q t < q s) : + paperProb q ε₁ ε₂ i = + Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) * + paperProb (lowerScore q s 1) ε₁ ε₂ i := by + have hmaxq : maxScore q = q s := maxScore_eq_of_unique_max q s huniq + have hgap_pos : 0 < gap q i := by + rw [gap_eq_maxScore_sub, hmaxq] + exact Nat.sub_pos_of_lt (huniq i his) + have hgap_one : 1 ≤ gap q i := Nat.succ_le_of_lt hgap_pos + unfold paperProb + rw [gap_lowerScore_other_of_unique_max_one q s i his huniq] + have hmul : + (gap q i * ε₁ : ℕ) = (gap q i - 1) * ε₁ + ε₁ := by + calc + gap q i * ε₁ = ((gap q i - 1) + 1) * ε₁ := by + rw [Nat.sub_add_cancel hgap_one] + _ = (gap q i - 1) * ε₁ + ε₁ := by ring + rw [hmul] + have hdiv : + (((((gap q i - 1) * ε₁ + ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) = + (((((gap q i - 1) * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) + + ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by + have hden : (((ε₂ : NNReal) : ℝ)) ≠ 0 := by positivity + have hnum : ((((gap q i - 1) * ε₁ + ε₁ : ℕ) : NNReal)) = + ((((gap q i - 1) * ε₁ : ℕ) : NNReal)) + ((ε₁ : ℕ) : NNReal) := by + exact_mod_cast (show (gap q i - 1) * ε₁ + ε₁ = (gap q i - 1) * ε₁ + ε₁ by rfl) + rw [hnum, NNReal.coe_div, NNReal.coe_div] + simp [add_div] + have hdiv' : + - (((((gap q i - 1) * ε₁ + ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) = + - ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) + + - (((((gap q i - 1) * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by + linarith + change + Real.exp (- (((((gap q i - 1) * ε₁ + ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) = + Real.exp (- ((((ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) * + Real.exp (- (((((gap q i - 1) * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) + rw [hdiv', Real.exp_add] + +theorem paperAlt_eq_paperAltGapZeroScaled_lowerScore_unique_max_one + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : r ≠ s) (huniq : ∀ t : Fin n.succ, t ≠ s → q t < q s) : + paperAlt q r ε₁ ε₂ = + paperAltGapZeroScaled (lowerScore q s 1) r s ε₁ ε₂ + (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) := by + have hs : gap q s = 0 := by + rw [gap_eq_maxScore_sub, maxScore_eq_of_unique_max q s huniq] + simp + rw [paperAlt_eq_sum_erase_gap_zero q r s ε₁ ε₂ hrs.symm hs] + unfold paperAltGapZeroScaled + apply Finset.sum_congr rfl + intro t ht + calc + (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + ∏ i ∈ t, paperProb q ε₁ ε₂ i + = (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + ∏ i ∈ t, + (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) * + paperProb (lowerScore q s 1) ε₁ ε₂ i) := by + congr 1 + apply Finset.prod_congr rfl + intro i hi + apply paperProb_lowerScore_other_of_unique_max_one + intro his + have : s ∈ ((Finset.univ.erase r).erase s) := (Finset.mem_powerset.mp ht) (his ▸ hi) + simp at this + exact huniq + _ = (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + ((∏ _i ∈ t, Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) * + ∏ i ∈ t, paperProb (lowerScore q s 1) ε₁ ε₂ i) := by + rw [Finset.prod_mul_distrib] + _ = (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + ((Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) ^ t.card) * + ∏ i ∈ t, paperProb (lowerScore q s 1) ε₁ ε₂ i) := by + rw [Finset.prod_const] + _ = (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂)) ^ t.card) * + ∏ i ∈ t, paperProb (lowerScore q s 1) ε₁ ε₂ i := by + ring + + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/Polynomials.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/Polynomials.lean new file mode 100644 index 00000000..57c51da8 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Paper/Polynomials.lean @@ -0,0 +1,507 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism.Core + +noncomputable section + +open scoped Classical +open PMF + +namespace SLang +namespace PermuteAndFlip +/-! +Paper polynomial and analytic lemmas for the paper-style proof. +-/ + +/-! ### The paper's real-valued quantities -/ + +theorem sum_powerset_neg_prod_eq_prod_one_sub + {α : Type} [DecidableEq α] (s : Finset α) (f : α → ℝ) : + Finset.sum s.powerset (fun t => Finset.prod t fun i => -f i) = + Finset.prod s (fun i => 1 - f i) := by + simpa [sub_eq_add_neg, add_comm] using + (Finset.prod_add (f := fun i => -f i) (g := fun _ => (1 : ℝ)) s).symm + +/-- +The paper's `p_i` term: the exact Bernoulli acceptance probability for +candidate `i`, viewed in `ℝ` rather than `ENNReal`. +-/ +def paperProb {n : CandidateCount} (q : Scores n) (ε₁ : ℕ) (ε₂ : ℕ+) (i : Fin n.succ) : ℝ := + Real.exp (- (((gap q i * ε₁ : ℕ) : NNReal) / ε₂)) + +/-- +The paper's alternating subset sum `A_r(q)`. Later modules show that this is +exactly the PMF mass on `r`, after factoring out the direct success term for `r`. +-/ +def paperAlt {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : ℝ := + Finset.sum (Finset.powerset (Finset.univ.erase r)) + (fun t => (((-1 : ℝ) ^ t.card) / (t.card + 1)) * Finset.prod t (paperProb q ε₁ ε₂)) + +/-- The scaled version of `paperAlt`, used when all non-`r` terms are multiplied by a common factor. -/ +def paperAltScaled {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : ℝ := + Finset.sum (Finset.powerset (Finset.univ.erase r)) + (fun t => (((-1 : ℝ) ^ t.card) / (t.card + 1)) * (c ^ t.card) * Finset.prod t (paperProb q ε₁ ε₂)) + +/-- +The paper primitive `c ↦ c * paperAltScaled ... c`. + +This is the analytic object whose derivative becomes a clean product +`∏ (1 - c * p_i)`, making monotonicity easy to prove on `[0,1]`. +-/ +def paperPrimitiveScaled {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : ℝ := + c * paperAltScaled q r ε₁ ε₂ c + +/-- +Reduced alternating sum for the gap-zero / maximizer case with one distinguished +extra candidate `s` removed. + +This is the polynomial that appears after splitting `paperAlt` into subsets that +do or do not contain a candidate with gap `0`. +-/ +def paperAltGapZeroScaled {n : CandidateCount} + (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : ℝ := + Finset.sum (Finset.powerset ((Finset.univ.erase r).erase s)) + (fun t => + (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + (c ^ t.card) * Finset.prod t (paperProb q ε₁ ε₂)) + +/-- +An antiderivative-like helper for `paperAltGapZeroScaled`. + +The extra factor `c^2` is chosen so that differentiating twice exposes the same +product structure as in the main paper polynomial argument. +-/ +def paperGapZeroDoublePrimitive {n : CandidateCount} + (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : ℝ := + c ^ 2 * paperAltGapZeroScaled q r s ε₁ ε₂ c + +/-- +The first derivative of `paperGapZeroDoublePrimitive`, written explicitly as a +finite sum. +-/ +def paperGapZeroPrimitive {n : CandidateCount} + (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : ℝ := + Finset.sum (Finset.powerset ((Finset.univ.erase r).erase s)) + (fun t => + (((-1 : ℝ) ^ t.card) / (t.card + 1)) * + (c ^ (t.card + 1)) * Finset.prod t (paperProb q ε₁ ε₂)) + +theorem paperAltScaled_one + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + paperAltScaled q r ε₁ ε₂ 1 = paperAlt q r ε₁ ε₂ := by + unfold paperAltScaled paperAlt + apply Finset.sum_congr rfl + intro t _ht + simp + +/-! ### Simplifying the maximizer case -/ + +theorem paperAlt_eq_sum_erase_gap_zero + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : s ≠ r) (hs : gap q s = 0) : + paperAlt q r ε₁ ε₂ = + Finset.sum (Finset.powerset ((Finset.univ.erase r).erase s)) + (fun t => + (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂)) := by + have hs_not_mem : s ∉ (Finset.univ.erase r).erase s := by simp + have hsplit : + (Finset.univ.erase r).powerset = + (((Finset.univ.erase r).erase s).powerset) ∪ + ((((Finset.univ.erase r).erase s).powerset).image (insert s)) := by + -- Split all subsets into those that omit `s` and those that contain it. + rw [← Finset.powerset_insert] + congr + ext x + simp [hrs] + rw [paperAlt, hsplit, Finset.sum_union] + · rw [Finset.sum_image] + · rw [← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro t ht + have hts : s ∉ t := by + intro hst + exact hs_not_mem ((Finset.mem_powerset.mp ht) hst) + have hcard : (insert s t).card = t.card + 1 := Finset.card_insert_of_notMem hts + have hprod : + Finset.prod (insert s t) (paperProb q ε₁ ε₂) = + Finset.prod t (paperProb q ε₁ ε₂) := by + rw [Finset.prod_insert hts] + unfold paperProb + simp [hs] + have hcoeff : + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) + + (((-1 : ℝ) ^ (t.card + 1)) / (t.card + 2))) = + (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) := by + -- Pair the "without `s`" and "with `s`" coefficients into the single + -- reduced coefficient used by `paperAltGapZeroScaled`. + have hne1 : ((t.card : ℝ) + 1) ≠ 0 := by positivity + have hne2 : ((t.card : ℝ) + 2) ≠ 0 := by positivity + field_simp [hne1, hne2] + ring + calc + (((-1 : ℝ) ^ t.card) / (t.card + 1)) * Finset.prod t (paperProb q ε₁ ε₂) + + (((-1 : ℝ) ^ (insert s t).card) / ((insert s t).card + 1)) * + Finset.prod (insert s t) (paperProb q ε₁ ε₂) + = + (((( -1 : ℝ) ^ t.card) / (t.card + 1)) + + (((-1 : ℝ) ^ (t.card + 1)) / (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂) := by + rw [hcard, hprod] + norm_num + ring + _ = (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂) := by + rw [hcoeff] + · intro a ha b hb hab + have ha_not : s ∉ a := by + intro hsa + exact hs_not_mem ((Finset.mem_powerset.mp ha) hsa) + have hb_not : s ∉ b := by + intro hsb + exact hs_not_mem ((Finset.mem_powerset.mp hb) hsb) + have h := congrArg (Finset.erase · s) hab + simpa [Finset.erase_insert, ha_not, hb_not] using h + · refine Finset.disjoint_left.mpr ?_ + intro t ht_left ht_right + rcases Finset.mem_image.mp ht_right with ⟨u, _hu, hut⟩ + have hs_mem : s ∈ t := by + rw [← hut] + simp + have hs_not : s ∉ t := by + intro hst + exact hs_not_mem ((Finset.mem_powerset.mp ht_left) hst) + exact hs_not hs_mem + +theorem paperAlt_eq_paperAltGapZeroScaled_one + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) + (hrs : s ≠ r) (hs : gap q s = 0) : + paperAlt q r ε₁ ε₂ = paperAltGapZeroScaled q r s ε₁ ε₂ 1 := by + rw [paperAlt_eq_sum_erase_gap_zero q r s ε₁ ε₂ hrs hs] + unfold paperAltGapZeroScaled + apply Finset.sum_congr rfl + intro t _ht + simp + +theorem paperGapZeroDoublePrimitive_eq_sum + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + paperGapZeroDoublePrimitive q r s ε₁ ε₂ = + fun c => + Finset.sum (Finset.powerset ((Finset.univ.erase r).erase s)) + (fun t => + (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + (c ^ (t.card + 2)) * Finset.prod t (paperProb q ε₁ ε₂)) := by + funext c + unfold paperGapZeroDoublePrimitive paperAltGapZeroScaled + -- Push the outer factor `c^2` inside the finite sum so that each summand is a + -- single power `c^(t.card + 2)`. + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro t _ht + rw [pow_add] + ring + +theorem paperPrimitiveScaled_eq_sum + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + paperPrimitiveScaled q r ε₁ ε₂ = + fun c => + Finset.sum (Finset.powerset (Finset.univ.erase r)) + (fun t => + (((-1 : ℝ) ^ t.card) / (t.card + 1)) * (c ^ (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂)) := by + funext c + unfold paperPrimitiveScaled paperAltScaled + -- Similarly, rewrite `c * paperAltScaled ... c` as a single power inside each summand. + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro t _ht + rw [pow_succ'] + ring + +theorem hasDerivAt_paperGapZeroDoublePrimitive + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : + HasDerivAt + (paperGapZeroDoublePrimitive q r s ε₁ ε₂) + (Finset.sum (Finset.powerset ((Finset.univ.erase r).erase s)) + (fun t => + (((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + ((t.card + 2 : ℝ) * c ^ (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂))) + c := by + rw [paperGapZeroDoublePrimitive_eq_sum] + have hsum : + HasDerivAt + (∑ t ∈ Finset.powerset ((Finset.univ.erase r).erase s), fun x : ℝ => + x ^ (t.card + 2) * + ((((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂))) + (Finset.sum (Finset.powerset ((Finset.univ.erase r).erase s)) + (fun t => + c ^ (t.card + 1) * (((t.card + 2 : ℝ)) * + ((((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂))))) + c := by + exact + (HasDerivAt.sum + (u := Finset.powerset ((Finset.univ.erase r).erase s)) + (A := fun t => fun x : ℝ => + x ^ (t.card + 2) * + ((((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂))) + (A' := fun t => + c ^ (t.card + 1) * (((t.card + 2 : ℝ)) * + ((((-1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂)))) + (x := c) + (fun (t : Finset (Fin n.succ)) _ht => by + have hpow : HasDerivAt (fun x : ℝ => x ^ (t.card + 2)) ((t.card + 2 : ℝ) * c ^ (t.card + 1)) c := by + simpa using hasDerivAt_pow (t.card + 2) c + simpa [mul_assoc, mul_left_comm, mul_comm] using + hpow.const_mul + (((( -1 : ℝ) ^ t.card) / ((t.card + 1) * (t.card + 2))) * + Finset.prod t (paperProb q ε₁ ε₂)))) + convert hsum using 1 + · ext x + simp [mul_assoc, mul_comm] + · simp [mul_assoc, mul_comm] + +theorem deriv_paperGapZeroDoublePrimitive_eq_paperGapZeroPrimitive + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : + deriv (paperGapZeroDoublePrimitive q r s ε₁ ε₂) c = + paperGapZeroPrimitive q r s ε₁ ε₂ c := by + rw [(hasDerivAt_paperGapZeroDoublePrimitive q r s ε₁ ε₂ c).deriv] + unfold paperGapZeroPrimitive + apply Finset.sum_congr rfl + intro t _ht + have ht1 : ((t.card : ℝ) + 1) ≠ 0 := by positivity + have ht2 : ((t.card : ℝ) + 2) ≠ 0 := by positivity + change + (((-1 : ℝ) ^ t.card) / (((t.card : ℝ) + 1) * ((t.card : ℝ) + 2)) * + (((t.card : ℝ) + 2) * c ^ (t.card + 1)) * Finset.prod t (paperProb q ε₁ ε₂)) = + (((-1 : ℝ) ^ t.card) / ((t.card : ℝ) + 1) * c ^ (t.card + 1) * + Finset.prod t (paperProb q ε₁ ε₂)) + field_simp [ht1, ht2] + +theorem hasDerivAt_paperGapZeroPrimitive + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : + HasDerivAt + (paperGapZeroPrimitive q r s ε₁ ε₂) + (Finset.prod ((Finset.univ.erase r).erase s) (fun i => 1 - c * paperProb q ε₁ ε₂ i)) + c := by + unfold paperGapZeroPrimitive + have hsum : + HasDerivAt + (∑ t ∈ Finset.powerset ((Finset.univ.erase r).erase s), fun x : ℝ => + x ^ (t.card + 1) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂))) + (Finset.sum (Finset.powerset ((Finset.univ.erase r).erase s)) + (fun t => + c ^ t.card * (((t.card + 1 : ℝ)) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂))))) + c := by + exact + (HasDerivAt.sum + (u := Finset.powerset ((Finset.univ.erase r).erase s)) + (A := fun t => fun x : ℝ => + x ^ (t.card + 1) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂))) + (A' := fun t => + c ^ t.card * (((t.card + 1 : ℝ)) * + ((((-1 : ℝ) ^ t.card) / (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂)))) + (x := c) + (fun (t : Finset (Fin n.succ)) _ht => by + have hpow : HasDerivAt (fun x : ℝ => x ^ (t.card + 1)) ((t.card + 1 : ℝ) * c ^ t.card) c := by + simpa using hasDerivAt_pow (t.card + 1) c + simpa [mul_assoc, mul_left_comm, mul_comm] using + hpow.const_mul + (((( -1 : ℝ) ^ t.card) / (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂)))) + have hderivEq : + Finset.sum ((Finset.univ.erase r).erase s).powerset + (fun t => (((-1 : ℝ) ^ t.card) / (t.card + 1)) * ((t.card + 1 : ℝ) * c ^ t.card) * + Finset.prod t (paperProb q ε₁ ε₂)) + = + Finset.prod ((Finset.univ.erase r).erase s) (fun i => 1 - c * paperProb q ε₁ ε₂ i) := by + calc + Finset.sum ((Finset.univ.erase r).erase s).powerset + (fun t => (((-1 : ℝ) ^ t.card) / (t.card + 1)) * ((t.card + 1 : ℝ) * c ^ t.card) * + Finset.prod t (paperProb q ε₁ ε₂)) + = Finset.sum ((Finset.univ.erase r).erase s).powerset + (fun t => (((-1 : ℝ) ^ t.card) * (c ^ t.card)) * Finset.prod t (paperProb q ε₁ ε₂)) := by + apply Finset.sum_congr rfl + intro t _ht + have hne : ((t.card : ℝ) + 1) ≠ 0 := by positivity + field_simp [hne] + _ = Finset.sum ((Finset.univ.erase r).erase s).powerset + (fun t => Finset.prod t (fun i => -(c * paperProb q ε₁ ε₂ i))) := by + apply Finset.sum_congr rfl + intro t _ht + have hpowneg : ((-c : ℝ) ^ t.card) = ((-1 : ℝ) ^ t.card) * c ^ t.card := by + rw [neg_eq_neg_one_mul, mul_pow] + calc + (((-1 : ℝ) ^ t.card) * (c ^ t.card)) * Finset.prod t (paperProb q ε₁ ε₂) + = ((-c : ℝ) ^ t.card) * Finset.prod t (paperProb q ε₁ ε₂) := by + rw [hpowneg] + _ = (Finset.prod t (fun _i => (-c : ℝ))) * Finset.prod t (paperProb q ε₁ ε₂) := by + rw [Finset.prod_const] + _ = Finset.prod t (fun i => ((-c : ℝ) * paperProb q ε₁ ε₂ i)) := by + rw [← Finset.prod_mul_distrib] + _ = Finset.prod t (fun i => -(c * paperProb q ε₁ ε₂ i)) := by + apply Finset.prod_congr rfl + intro i _hi + ring + _ = Finset.prod ((Finset.univ.erase r).erase s) (fun i => 1 - c * paperProb q ε₁ ε₂ i) := by + exact sum_powerset_neg_prod_eq_prod_one_sub (((Finset.univ.erase r).erase s)) (fun i => c * paperProb q ε₁ ε₂ i) + convert hsum using 1 + · ext x + simp [mul_assoc, mul_comm] + · simpa [mul_assoc, mul_left_comm, mul_comm] using hderivEq.symm + +theorem paperGapZeroPrimitive_monotoneOn_Icc + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + MonotoneOn (paperGapZeroPrimitive q r s ε₁ ε₂) (Set.Icc (0 : ℝ) 1) := by + have hdiff : Differentiable ℝ (paperGapZeroPrimitive q r s ε₁ ε₂) := by + intro x + exact (hasDerivAt_paperGapZeroPrimitive q r s ε₁ ε₂ x).differentiableAt + refine monotoneOn_of_deriv_nonneg (convex_Icc (0 : ℝ) 1) + hdiff.continuous.continuousOn hdiff.differentiableOn ?_ + intro x hx + rw [interior_Icc] at hx + rcases hx with ⟨hx0, hx1⟩ + rw [(hasDerivAt_paperGapZeroPrimitive q r s ε₁ ε₂ x).deriv] + apply Finset.prod_nonneg + intro i _hi + have hpi0 : 0 ≤ paperProb q ε₁ ε₂ i := by + unfold paperProb + positivity + have hpi1 : paperProb q ε₁ ε₂ i ≤ 1 := by + unfold paperProb + have hnonneg : 0 ≤ ((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ) := by + positivity + have hle : Real.exp (-((((gap q i * ε₁ : ℕ) : NNReal) / ε₂ : NNReal) : ℝ)) ≤ Real.exp 0 := by + refine Real.exp_le_exp.mpr ?_ + linarith + simpa using hle + have hmul : 0 ≤ x * paperProb q ε₁ ε₂ i ∧ x * paperProb q ε₁ ε₂ i ≤ 1 := by + constructor + · exact mul_nonneg hx0.le hpi0 + · have _hxle : x ≤ 1 := hx1.le + nlinarith + linarith + +theorem paperGapZeroDoublePrimitive_convexOn_Icc + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + ConvexOn ℝ (Set.Icc (0 : ℝ) 1) (paperGapZeroDoublePrimitive q r s ε₁ ε₂) := by + have hcont : + ContinuousOn (paperGapZeroDoublePrimitive q r s ε₁ ε₂) (Set.Icc (0 : ℝ) 1) := by + have hdiff : Differentiable ℝ (paperGapZeroDoublePrimitive q r s ε₁ ε₂) := by + intro x + exact (hasDerivAt_paperGapZeroDoublePrimitive q r s ε₁ ε₂ x).differentiableAt + exact hdiff.continuous.continuousOn + have hderiv : + DifferentiableOn ℝ (paperGapZeroDoublePrimitive q r s ε₁ ε₂) (interior (Set.Icc (0 : ℝ) 1)) := by + intro x _hx + exact (hasDerivAt_paperGapZeroDoublePrimitive q r s ε₁ ε₂ x).differentiableAt.differentiableWithinAt + have hmono : + MonotoneOn (deriv (paperGapZeroDoublePrimitive q r s ε₁ ε₂)) (interior (Set.Icc (0 : ℝ) 1)) := by + rw [show interior (Set.Icc (0 : ℝ) 1) = Set.Ioo (0 : ℝ) 1 by rw [interior_Icc]] + intro x hx y hy hxy + rw [deriv_paperGapZeroDoublePrimitive_eq_paperGapZeroPrimitive, + deriv_paperGapZeroDoublePrimitive_eq_paperGapZeroPrimitive] + exact paperGapZeroPrimitive_monotoneOn_Icc q r s ε₁ ε₂ + (show x ∈ Set.Icc (0 : ℝ) 1 by exact ⟨hx.1.le, hx.2.le⟩) + (show y ∈ Set.Icc (0 : ℝ) 1 by exact ⟨hy.1.le, hy.2.le⟩) + hxy + exact hmono.convexOn_of_deriv + (convex_Icc (0 : ℝ) 1) + hcont + hderiv + +theorem paperGapZeroDoublePrimitive_monotoneOn_Icc + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + MonotoneOn (paperGapZeroDoublePrimitive q r s ε₁ ε₂) (Set.Icc (0 : ℝ) 1) := by + have hdiff : Differentiable ℝ (paperGapZeroDoublePrimitive q r s ε₁ ε₂) := by + intro x + exact (hasDerivAt_paperGapZeroDoublePrimitive q r s ε₁ ε₂ x).differentiableAt + refine monotoneOn_of_deriv_nonneg (convex_Icc (0 : ℝ) 1) + hdiff.continuous.continuousOn hdiff.differentiableOn ?_ + intro x hx + rw [interior_Icc] at hx + have hx' : x ∈ Set.Icc (0 : ℝ) 1 := ⟨hx.1.le, hx.2.le⟩ + rw [deriv_paperGapZeroDoublePrimitive_eq_paperGapZeroPrimitive] + have hmono := paperGapZeroPrimitive_monotoneOn_Icc q r s ε₁ ε₂ + have h0x := hmono (by simp) hx' hx.1.le + have hzero : paperGapZeroPrimitive q r s ε₁ ε₂ 0 = 0 := by + simp [paperGapZeroPrimitive] + linarith + +theorem paperAltGapZeroScaled_mul_le_paperAltGapZero + {n : CandidateCount} (q : Scores n) (r s : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) {c : ℝ} + (hc0 : 0 ≤ c) (hc1 : c ≤ 1) : + c * paperAltGapZeroScaled q r s ε₁ ε₂ c ≤ paperAltGapZeroScaled q r s ε₁ ε₂ 1 := by + have hconv := paperGapZeroDoublePrimitive_convexOn_Icc q r s ε₁ ε₂ + have hc : c ∈ Set.Icc (0 : ℝ) 1 := ⟨hc0, hc1⟩ + have h1 : (1 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := by simp + by_cases hcz : c = 0 + · subst hcz + have hmono := paperGapZeroDoublePrimitive_monotoneOn_Icc q r s ε₁ ε₂ + have h01 := hmono + (show (0 : ℝ) ∈ Set.Icc (0 : ℝ) 1 by simp) + (show (1 : ℝ) ∈ Set.Icc (0 : ℝ) 1 by simp) + (show (0 : ℝ) ≤ 1 by norm_num) + simpa [paperGapZeroDoublePrimitive] using h01 + · have hsec := + hconv.secant_mono + (by simp) + hc + h1 + hcz + (by norm_num) + hc1 + have hzero : paperGapZeroDoublePrimitive q r s ε₁ ε₂ 0 = 0 := by + simp [paperGapZeroDoublePrimitive] + have hc_eq : + (paperGapZeroDoublePrimitive q r s ε₁ ε₂ c - + paperGapZeroDoublePrimitive q r s ε₁ ε₂ 0) / (c - 0) = + c * paperAltGapZeroScaled q r s ε₁ ε₂ c := by + rw [hzero] + calc + (paperGapZeroDoublePrimitive q r s ε₁ ε₂ c - 0) / (c - 0) + = (c ^ 2 * paperAltGapZeroScaled q r s ε₁ ε₂ c) / c := by + simp [paperGapZeroDoublePrimitive] + _ = c * paperAltGapZeroScaled q r s ε₁ ε₂ c := by + field_simp [hcz] + have h1_eq : + (paperGapZeroDoublePrimitive q r s ε₁ ε₂ 1 - + paperGapZeroDoublePrimitive q r s ε₁ ε₂ 0) / (1 - 0) = + paperAltGapZeroScaled q r s ε₁ ε₂ 1 := by + simp [paperGapZeroDoublePrimitive] + rw [hc_eq, h1_eq] at hsec + exact hsec + + +def paperPrimitivePoly {n : CandidateCount} + (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) (c : ℝ) : ℝ := + Finset.sum (Finset.powerset (Finset.univ.erase r)) + (fun t => (((-1 : ℝ) ^ t.card) / (t.card + 1)) * (c ^ (t.card + 1)) * + Finset.prod t (paperProb q ε₁ ε₂)) + +@[simp] +theorem paperPrimitiveScaled_eq_paperPrimitivePoly + {n : CandidateCount} (q : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + paperPrimitiveScaled q r ε₁ ε₂ = paperPrimitivePoly q r ε₁ ε₂ := by + funext c + simp [paperPrimitivePoly, paperPrimitiveScaled_eq_sum] + + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Peeling.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Peeling.lean new file mode 100644 index 00000000..bca81031 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Peeling.lean @@ -0,0 +1,297 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Privacy + +noncomputable section + +open scoped Classical + +namespace SLang +namespace PermuteAndFlip + +abbrev ScoreMechanism (n : CandidateCount) (U : Type) := Scores n → SLang U + +/-- Adaptive composition, written directly in pointwise form. -/ +def scoreComposeAdaptive {n : CandidateCount} + (m₁ : ScoreMechanism n U) (m₂ : U → ScoreMechanism n V) : + ScoreMechanism n (U × V) := + fun q uv => m₁ q uv.1 * m₂ uv.1 q uv.2 + +/-- Postprocessing, written as the fiberwise pushforward of a distribution. -/ +def scorePostprocess {n : CandidateCount} + (m : ScoreMechanism n U) (f : U → V) : + ScoreMechanism n V := + fun q v => ∑' u : U, if f u = v then m q u else 0 + +/-- Pointwise privacy under the range metric, with budget `steps`. -/ +def RangePrivate {n : CandidateCount} (α : ENNReal) (steps : ℕ) + (m : ScoreMechanism n U) : Prop := + ∀ q q' u, + α ^ (steps * rangeDistance q q') * m q u ≤ m q' u + +namespace RangePrivate + +@[simp] theorem const {n : CandidateCount} (α : ENNReal) (u : U) : + RangePrivate α 0 (fun _ : Scores n => SLang.probPure u) := by + intro q q' x + simp [SLang.probPure] + +theorem const_of_le_one {n : CandidateCount} {α : ENNReal} {steps : ℕ} + (hα : α ≤ 1) (u : U) : + RangePrivate α steps (fun _ : Scores n => SLang.probPure u) := by + intro q q' x + by_cases hx : x = u + · subst hx + have hpow : α ^ (steps * rangeDistance q q') ≤ 1 := by + exact pow_le_one' hα _ + simpa [SLang.probPure] using hpow + · simp [SLang.probPure, hx] + +@[simp] theorem composeAdaptive {n : CandidateCount} + {α : ENNReal} {s₁ s₂ : ℕ} + {m₁ : ScoreMechanism n U} {m₂ : U → ScoreMechanism n V} + (h₁ : RangePrivate α s₁ m₁) + (h₂ : ∀ u, RangePrivate α s₂ (m₂ u)) : + RangePrivate α (s₁ + s₂) (scoreComposeAdaptive m₁ m₂) := by + intro q q' uv + rcases uv with ⟨u, v⟩ + let d := rangeDistance q q' + have hm₁ := h₁ q q' u + have hm₂ := h₂ u q q' v + calc + α ^ ((s₁ + s₂) * d) * scoreComposeAdaptive m₁ m₂ q (u, v) + = (α ^ (s₁ * d) * m₁ q u) * (α ^ (s₂ * d) * m₂ u q v) := by + simp [scoreComposeAdaptive, d, Nat.add_mul, pow_add, + mul_assoc, mul_left_comm, mul_comm] + _ ≤ m₁ q' u * m₂ u q' v := by + exact mul_le_mul' hm₁ hm₂ + _ = scoreComposeAdaptive m₁ m₂ q' (u, v) := by + simp [scoreComposeAdaptive] + +@[simp] theorem postprocess {n : CandidateCount} + {α : ENNReal} {steps : ℕ} + {m : ScoreMechanism n U} (h : RangePrivate α steps m) + (f : U → V) : + RangePrivate α steps (scorePostprocess m f) := by + intro q q' v + let γ := α ^ (steps * rangeDistance q q') + calc + γ * scorePostprocess m f q v + = γ * ∑' u : U, if f u = v then m q u else 0 := by + simp [scorePostprocess] + _ = ∑' u : U, γ * (if f u = v then m q u else 0) := by + symm + exact ENNReal.tsum_mul_left + _ = ∑' u : U, if f u = v then m q u * γ else 0 := by + refine tsum_congr ?_ + intro u + by_cases hu : f u = v + · simp [hu, mul_comm] + · simp [hu] + _ ≤ ∑' u : U, if f u = v then m q' u else 0 := by + apply ENNReal.tsum_le_tsum + intro u + by_cases hu : f u = v + · simpa [hu, γ, mul_assoc, mul_left_comm, mul_comm] using h q q' u + · simp [hu] + _ = scorePostprocess m f q' v := by + simp [scorePostprocess] + +end RangePrivate + +/-- `privacyBase` is always at most `1`, so larger exponents only make the factor smaller. -/ +lemma privacyBase_le_one (ε₁ : ℕ) (ε₂ : ℕ+) : privacyBase ε₁ ε₂ ≤ 1 := by + dsimp [privacyBase] + refine ENNReal.ofReal_le_one.mpr ?_ + have hnonpos : -((((ε₁ : ℕ) : NNReal) / ε₂ : ℝ)) ≤ 0 := by + have hnonneg : 0 ≤ ((((ε₁ : ℕ) : NNReal) / ε₂ : ℝ)) := by positivity + linarith + exact Real.exp_le_one_iff.mpr hnonpos + +lemma privacyBase_pow_antitone {ε₁ : ℕ} {ε₂ : ℕ+} {a b : ℕ} + (h : a ≤ b) : + privacyBase ε₁ ε₂ ^ b ≤ privacyBase ε₁ ε₂ ^ a := by + obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le h + calc + privacyBase ε₁ ε₂ ^ (a + c) + = privacyBase ε₁ ε₂ ^ a * privacyBase ε₁ ε₂ ^ c := by + rw [pow_add] + _ ≤ privacyBase ε₁ ε₂ ^ a * 1 := by + exact mul_le_mul_right (pow_le_one' (privacyBase_le_one ε₁ ε₂) c) _ + _ = privacyBase ε₁ ε₂ ^ a := by simp + +/-- Restrict a score vector to the candidates listed in `l`. -/ +def restrictScores {n : CandidateCount} (q : Scores n) + (l : List (Fin n.succ)) (hl : l ≠ []) : Scores (l.length - 1) := + fun i => + let hi : i.val < l.length := by + have hpos : 0 < l.length := List.length_pos_iff_ne_nil.mpr hl + have hi0 : i.val < (l.length - 1).succ := i.is_lt + omega + q (l.get ⟨i.val, hi⟩) + +/-- Lift an index in the restricted list back to the original candidate space. -/ +def liftFromList {n : CandidateCount} + (l : List (Fin n.succ)) (hl : l ≠ []) : + Fin (l.length - 1).succ → Fin n.succ := + fun i => + let hi : i.val < l.length := by + have hpos : 0 < l.length := List.length_pos_iff_ne_nil.mpr hl + have hi0 : i.val < (l.length - 1).succ := i.is_lt + omega + l.get ⟨i.val, hi⟩ + +@[simp] lemma restrictScores_eq_comp_lift {n : CandidateCount} + (q : Scores n) (l : List (Fin n.succ)) (hl : l ≠ []) : + restrictScores q l hl = fun i => q (liftFromList l hl i) := by + rfl + +/-- Removing coordinates cannot increase the range metric. -/ +lemma rangeDistance_restrict_le {n : CandidateCount} + (q q' : Scores n) (l : List (Fin n.succ)) (hl : l ≠ []) : + rangeDistance (restrictScores q l hl) (restrictScores q' l hl) + ≤ rangeDistance q q' := by + let qr : Scores (l.length - 1) := restrictScores q l hl + let qr' : Scores (l.length - 1) := restrictScores q' l hl + have hmin : RangePrivacy.diffMin q q' ≤ RangePrivacy.diffMin qr qr' := by + have hmem : RangePrivacy.diffMin qr qr' ∈ RangePrivacy.diffSet qr qr' := + Finset.min'_mem _ _ + rcases Finset.mem_image.mp hmem with ⟨i, -, hi⟩ + rw [← hi] + simpa [qr, qr', restrictScores_eq_comp_lift] using + (RangePrivacy.scoreDiff_mem_interval q q' (liftFromList l hl i)).1 + have hmax : RangePrivacy.diffMax qr qr' ≤ RangePrivacy.diffMax q q' := by + have hmem : RangePrivacy.diffMax qr qr' ∈ RangePrivacy.diffSet qr qr' := + Finset.max'_mem _ _ + rcases Finset.mem_image.mp hmem with ⟨i, -, hi⟩ + rw [← hi] + simpa [qr, qr', restrictScores_eq_comp_lift] using + (RangePrivacy.scoreDiff_mem_interval q q' (liftFromList l hl i)).2 + have hle : + RangePrivacy.diffMax qr qr' - RangePrivacy.diffMin qr qr' + ≤ RangePrivacy.diffMax q q' - RangePrivacy.diffMin q q' := by + linarith + dsimp [rangeDistance] + exact Int.toNat_le_toNat hle + +/-- Permute-and-flip on a fixed remaining candidate list, followed by the deterministic +map back to original candidate labels. -/ +def subsetPermuteAndFlipSLang {n : CandidateCount} + (l : List (Fin n.succ)) (hl : l ≠ []) + (ε₁ : ℕ) (ε₂ : ℕ+) : + ScoreMechanism n (Fin n.succ) := + scorePostprocess + (fun q => permuteAndFlipSLang (l.length - 1) (restrictScores q l hl) ε₁ ε₂) + (liftFromList l hl) + +lemma subsetPermuteAndFlip_range_private {n : CandidateCount} + (l : List (Fin n.succ)) (hl : l ≠ []) + (ε₁ : ℕ) (ε₂ : ℕ+) : + RangePrivate (privacyBase ε₁ ε₂) 1 (subsetPermuteAndFlipSLang l hl ε₁ ε₂) := by + let α := privacyBase ε₁ ε₂ + have hcore : RangePrivate α 1 + (fun q => permuteAndFlipSLang (l.length - 1) (restrictScores q l hl) ε₁ ε₂) := by + intro q q' r + let d := rangeDistance q q' + let dr := rangeDistance (restrictScores q l hl) (restrictScores q' l hl) + have hpf : α ^ dr * + permuteAndFlipSLang (l.length - 1) (restrictScores q l hl) ε₁ ε₂ r + ≤ + permuteAndFlipSLang (l.length - 1) (restrictScores q' l hl) ε₁ ε₂ r := by + simpa [α, dr] using + permuteAndFlipSLang_range_privacy + (q := restrictScores q l hl) + (q' := restrictScores q' l hl) + (r := r) (ε₁ := ε₁) (ε₂ := ε₂) + have hdr : dr ≤ d := rangeDistance_restrict_le q q' l hl + have hpow : α ^ d ≤ α ^ dr := privacyBase_pow_antitone (ε₁ := ε₁) (ε₂ := ε₂) hdr + have hmul : α ^ d * + permuteAndFlipSLang (l.length - 1) (restrictScores q l hl) ε₁ ε₂ r + ≤ + α ^ dr * permuteAndFlipSLang (l.length - 1) (restrictScores q l hl) ε₁ ε₂ r := by + exact mul_le_mul_left hpow _ + have hfinal : α ^ (1 * rangeDistance q q') * + permuteAndFlipSLang (l.length - 1) (restrictScores q l hl) ε₁ ε₂ r + ≤ + permuteAndFlipSLang (l.length - 1) (restrictScores q' l hl) ε₁ ε₂ r := by + simpa [d] using le_trans hmul hpf + exact hfinal + simpa [subsetPermuteAndFlipSLang] using RangePrivate.postprocess hcore (liftFromList l hl) + +/-- Peeling permute-and-flip over a list of remaining candidates. -/ +def peelPermuteAndFlipSLangAux {n : CandidateCount} + (l : List (Fin n.succ)) (k : ℕ) (ε₁ : ℕ) (ε₂ : ℕ+) : + ScoreMechanism n (List (Fin n.succ)) := + match k with + | 0 => fun _ => SLang.probPure [] + | k + 1 => + match l with + | [] => fun _ => SLang.probPure [] + | a :: as => + scorePostprocess + (scoreComposeAdaptive + (subsetPermuteAndFlipSLang (a :: as) (by simp) ε₁ ε₂) + (fun r => peelPermuteAndFlipSLangAux ((a :: as).erase r) k ε₁ ε₂)) + (fun z => z.1 :: z.2) + +/-- Top-level peeling mechanism: start from the canonical candidate order. -/ +def peelPermuteAndFlipSLang (n : CandidateCount) + (k : ℕ) (ε₁ : ℕ) (ε₂ : ℕ+) : + ScoreMechanism n (List (Fin n.succ)) := + peelPermuteAndFlipSLangAux (canonicalOrder n) k ε₁ ε₂ + +theorem peelPermuteAndFlipSLangAux_range_private {n : CandidateCount} : + ∀ (l : List (Fin n.succ)), l.Nodup → ∀ (k : ℕ) (ε₁ : ℕ) (ε₂ : ℕ+), + RangePrivate (privacyBase ε₁ ε₂) k + (peelPermuteAndFlipSLangAux l k ε₁ ε₂) := by + intro l hl k + induction k generalizing l with + | zero => + intro ε₁ ε₂ q q' ys + by_cases hys : ys = [] <;> + simp [peelPermuteAndFlipSLangAux, SLang.probPure, hys] + | succ k ih => + intro ε₁ ε₂ + cases l with + | nil => + simpa [peelPermuteAndFlipSLangAux] using + (RangePrivate.const_of_le_one + (α := privacyBase ε₁ ε₂) + (steps := k + 1) + (privacyBase_le_one ε₁ ε₂) + ([] : List (Fin n.succ))) + | cons a as => + have hhead : RangePrivate (privacyBase ε₁ ε₂) 1 + (subsetPermuteAndFlipSLang (a :: as) (by simp) ε₁ ε₂) := + subsetPermuteAndFlip_range_private (a :: as) (by simp) ε₁ ε₂ + have htail : ∀ r, + RangePrivate (privacyBase ε₁ ε₂) k + (peelPermuteAndFlipSLangAux ((a :: as).erase r) k ε₁ ε₂) := by + intro r + exact ih ((a :: as).erase r) (hl.erase r) ε₁ ε₂ + simpa [peelPermuteAndFlipSLangAux, Nat.add_comm] using + RangePrivate.postprocess + (RangePrivate.composeAdaptive hhead htail) + (fun z : Fin n.succ × List (Fin n.succ) => z.1 :: z.2) + +/-- Privacy theorem for peeling permute-and-flip. The budget grows linearly in `k`, +matching the OpenDP implementation's composition accounting. -/ +theorem peelPermuteAndFlipSLang_range_privacy {n : CandidateCount} + (q q' : Scores n) (ys : List (Fin n.succ)) + (k : ℕ) (ε₁ : ℕ) (ε₂ : ℕ+) : + (privacyBase ε₁ ε₂) ^ (k * rangeDistance q q') * + peelPermuteAndFlipSLang n k ε₁ ε₂ q ys + ≤ + peelPermuteAndFlipSLang n k ε₁ ε₂ q' ys := by + simpa [peelPermuteAndFlipSLang] using + peelPermuteAndFlipSLangAux_range_private + (l := canonicalOrder n) + (by simpa [canonicalOrder] using List.nodup_finRange n.succ) + (k := k) (ε₁ := ε₁) (ε₂ := ε₂) + q q' ys + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Privacy.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Privacy.lean new file mode 100644 index 00000000..5ffaf154 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Privacy.lean @@ -0,0 +1,125 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Range +import SampCert.DifferentialPrivacy.PermuteAndFlip.Monotonicity + +/-! +Final privacy-facing theorems for permute-and-flip. + +Main theorems in this file: +- `permuteAndFlipPMF_normalized_range_privacy`: normalized comparison after + shifting score differences into a common natural interval +- `permuteAndFlipPMF_range_privacy`: final PMF privacy theorem +- `permuteAndFlipSLang_range_privacy`: exact-sampler refinement of the PMF theorem +-/ + +noncomputable section + +namespace SLang +namespace PermuteAndFlip + +/-- +The per-unit privacy contraction factor `exp(-ε₁ / ε₂)` that appears throughout the +range-distance theorems below. +-/ +def privacyBase (ε₁ : ℕ) (ε₂ : ℕ+) : ENNReal := + ENNReal.ofReal (Real.exp (- (((ε₁ : ℕ) : NNReal) / ε₂))) + +/-- +Normalized privacy comparison after shifting both score vectors into a common +natural-valued interval. + +After normalization, the proof uses the `k`-step bump contraction and then +global monotonicity. +-/ +theorem permuteAndFlipPMF_normalized_range_privacy + {n : CandidateCount} (q q' : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + let B := RangePrivacy.upperEndpoint q q' + let qshift : Scores n := fun i => q i + B + let qtarget : Scores n := fun i => q i + RangePrivacy.shiftedDiff q q' i + (privacyBase ε₁ ε₂) ^ rangeDistance q q' * permuteAndFlipPMF n qshift ε₁ ε₂ r ≤ + permuteAndFlipPMF n qtarget ε₁ ε₂ r := by + let A := RangePrivacy.lowerEndpoint q q' + let B := RangePrivacy.upperEndpoint q q' + let qshift : Scores n := fun i => q i + B + let qmid : Scores n := fun i => q i + if i = r then A else B + let qtarget : Scores n := fun i => q i + RangePrivacy.shiftedDiff q q' i + have hred : + (privacyBase ε₁ ε₂) ^ rangeDistance q q' * permuteAndFlipPMF n qshift ε₁ ε₂ r ≤ + permuteAndFlipPMF n qmid ε₁ ε₂ r := by + -- `qshift` is obtained from `qmid` by raising only candidate `r` by exactly + -- the width of the normalized interval, so `bumpScore_self_privacy_pow` applies. + have hbump : bumpScore qmid r (rangeDistance q q') = qshift := by + funext i + by_cases hi : i = r + · subst hi + simp [qmid, qshift, A, B, RangePrivacy.upperEndpoint_eq_lowerEndpoint_add_rangeDistance, + bumpScore, Nat.add_assoc] + · simp [qmid, qshift, bumpScore, hi] + simpa [privacyBase, hbump] using + (bumpScore_self_privacy_pow (q := qmid) (r := r) (k := rangeDistance q q') + (ε₁ := ε₁) (ε₂ := ε₂)) + have hmono : + permuteAndFlipPMF n qmid ε₁ ε₂ r ≤ + permuteAndFlipPMF n qtarget ε₁ ε₂ r := by + -- After the bump step, every coordinate of `qtarget` lies between the same + -- normalized endpoints, so global monotonicity finishes the comparison. + apply permuteAndFlipPMF_monotone (q := qmid) (q' := qtarget) (r := r) (ε₁ := ε₁) (ε₂ := ε₂) + · have hle := RangePrivacy.lowerEndpoint_le_shiftedDiff q q' r + simpa [qmid, qtarget, A] using Nat.add_le_add_left hle (q r) + · intro s hsr + have hle := RangePrivacy.shiftedDiff_le_upperEndpoint q q' s + simpa [qmid, qtarget, B, hsr] using Nat.add_le_add_left hle (q s) + exact le_trans hred hmono + +/-- +Final PMF privacy theorem for permute-and-flip under the range metric. + +This is the development's main analogue of the paper's privacy theorem +(Theorem 1), phrased using `rangeDistance` instead of the paper's original +score-function presentation. +-/ +theorem permuteAndFlipPMF_range_privacy + {n : CandidateCount} (q q' : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + (privacyBase ε₁ ε₂) ^ rangeDistance q q' * permuteAndFlipPMF n q ε₁ ε₂ r ≤ + permuteAndFlipPMF n q' ε₁ ε₂ r := by + -- Shift both score vectors so that their coordinatewise differences become a + -- common natural-valued interval. The normalized theorem handles the real + -- work, and shift-invariance transports the result back to the original scores. + let B := RangePrivacy.upperEndpoint q q' + let c := RangePrivacy.diffShift q q' + let qshift : Scores n := fun i => q i + B + let qtarget : Scores n := fun i => q i + RangePrivacy.shiftedDiff q q' i + have htarget : + qtarget = (fun i => q' i + c) := by + -- By construction, `shiftedDiff` reconstructs `q'` up to a global shift. + simpa [qtarget, c] using RangePrivacy.shiftedDiff_eq_targetShift q q' + calc + (privacyBase ε₁ ε₂) ^ rangeDistance q q' * permuteAndFlipPMF n q ε₁ ε₂ r + = (privacyBase ε₁ ε₂) ^ rangeDistance q q' * permuteAndFlipPMF n qshift ε₁ ε₂ r := by + -- Replace `q` by its globally shifted copy `qshift`. + rw [permuteAndFlipPMF_shift (q := q) (c := B) (ε₁ := ε₁) (ε₂ := ε₂) (r := r)] + _ ≤ permuteAndFlipPMF n qtarget ε₁ ε₂ r := by + simpa [qshift, qtarget] using + permuteAndFlipPMF_normalized_range_privacy (q := q) (q' := q') (r := r) (ε₁ := ε₁) (ε₂ := ε₂) + _ = permuteAndFlipPMF n q' ε₁ ε₂ r := by + -- Remove the global shift on the target side. + rw [htarget, permuteAndFlipPMF_shift (q := q') (c := c) (ε₁ := ε₁) (ε₂ := ε₂) (r := r)] + +/-- +Final PMF privacy theorem for permute-and-flip under the range metric. + +This theorem is the `SLang` refinement of `permuteAndFlipPMF_range_privacy`. +-/ +theorem permuteAndFlipSLang_range_privacy + {n : CandidateCount} (q q' : Scores n) (r : Fin n.succ) (ε₁ : ℕ) (ε₂ : ℕ+) : + (privacyBase ε₁ ε₂) ^ rangeDistance q q' * permuteAndFlipSLang n q ε₁ ε₂ r ≤ + permuteAndFlipSLang n q' ε₁ ε₂ r := by + simpa [permuteAndFlipSLang_eq_permuteAndFlipPMF] using + permuteAndFlipPMF_range_privacy q q' r ε₁ ε₂ + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/README.md b/SampCert/DifferentialPrivacy/PermuteAndFlip/README.md new file mode 100644 index 00000000..c86a8339 --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/README.md @@ -0,0 +1,97 @@ +# Permute-and-Flip in SampCert + +A Lean formalization of the permute-and-flip selection mechanism of McKenna and +Sheldon, ["Permute-and-Flip: A New Mechanism for Differentially Private +Selection"](https://arxiv.org/abs/2010.12603). The development starts from the +mathematical mechanism and refines it down to an exact `SLang` implementation +built on SampCert's Bernoulli-negative-exponential sampler. + +## Results + +The two exported theorems live in `Privacy.lean`: + +- `permuteAndFlipPMF_range_privacy`, privacy of the mechanism's PMF; +- `permuteAndFlipSLang_range_privacy`, the same guarantee for the executable + `SLang` implementation. + +Both are stated in terms of the range distance between score vectors, + + rangeDistance q q' = max_i (q' i - q i) - min_i (q' i - q i), + +rather than a symmetric `[-1, 1]` perturbation. Stating privacy directly on the +score vectors keeps the final API free of an extra score-function abstraction, +and it gives tighter accounting when the score changes are monotone and differ +by a common shift. + +Reaching those theorems requires a closed form for the PMF, the monotonicity and +regularity properties the privacy argument depends on, and the refinement +theorem tying the `SLang` implementation back to the PMF. + +## Files + +`Basic.lean` is a facade that pulls in the development and carries the +paper-to-code map. `Privacy.lean` holds the final theorems and is the place to +start. + +The privacy argument is spread across: + +- `Range.lean`, the range metric and the normalization gadgets used by the proof; +- `MonotonicityLocal.lean`, the one-coordinate lemmas for raising the selected + candidate and lowering a competitor, including the delicate unique-max case; +- `Monotonicity.lean`, which assembles those into shift invariance, global + monotonicity, and the one- and `k`-step privacy contractions; +- `Reduction.lean`, a standalone abstract reduction from regularity to privacy + on integer-valued score vectors, with interval and range-distance + generalizations (namespace `SLang.PermuteAndFlip.Reduction`). + +The mechanism itself lives in `Mechanism/`: + +- `Core.lean`, the score transforms, gaps, recursive selector, and exact sampler; +- `SelectorCore.lean`, selector weights and canonical-order lemmas for a fixed + candidate order; +- `Selector.lean`, the mechanism as an average over uniform random permutations. + +The paper-style closed form lives in `Paper/`: + +- `Polynomials.lean`, the paper's real-valued quantities (`paperProb`, + `paperAlt`, and their variants); +- `Counting.lean`, the permutation-counting facts behind the `1 / (|t| + 1)` + coefficient; +- `ClosedForm.lean`, which identifies the mechanism's PMF with the paper's + alternating subset sum. + +## The mechanism + +Operationally, permute-and-flip + +1. samples a uniform random permutation of the candidates, +2. scans them in that order, +3. accepts candidate `i` with probability `exp(-gap(q, i) * ε₁ / ε₂)`, +4. and returns the first accepted candidate. + +The `Mechanism` files develop this operational form. The `Paper` files develop +the alternative closed-form PMF: the permutation average is rewritten using +`beforeSet`, the subset-event coefficient is computed by combinatorics, and the +resulting expression is matched to the paper's alternating subset polynomial. + +## The privacy proof + +`Privacy.lean` works in three steps. Given score vectors `q` and `q'`, the +coordinatewise differences `q' i - q i` may be negative, so they are shifted by a +common constant into a natural-valued interval `[A, B]` whose width is exactly +`rangeDistance q q'`. The proof then compares the normalized target vector +against the vector sitting at the upper endpoint `B` in every coordinate except +the chosen candidate `r`, which sits at `A`. That comparison factors into a +`k`-step contraction that repeatedly raises `r`, together with a monotonicity +argument showing that raising `r` while lowering the others can only favor `r`. +Since the mechanism is shift-invariant, the normalized comparison transfers back +to the original `q` and `q'`. + +## Paper-to-code map + +- Proposition 2, the regularity reduction: `Reduction.reduced_privacy_of_regular` +- Closed-form PMF: `Paper.ClosedForm.permuteAndFlipPMF_eq_ofReal_paperProb_mul_paperAlt` +- Concrete monotonicity / regularity: `Monotonicity.permuteAndFlipPMF_monotone` +- One-step privacy contraction: `Monotonicity.one_step_privacy` +- Final PMF privacy theorem: `Privacy.permuteAndFlipPMF_range_privacy` +- Exact implementation refinement: `Privacy.permuteAndFlipSLang_range_privacy` diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Range.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Range.lean new file mode 100644 index 00000000..87a7b73e --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Range.lean @@ -0,0 +1,151 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import SampCert.DifferentialPrivacy.PermuteAndFlip.Mechanism.Core + +/-! +Range-distance layer for permute-and-flip. + +This module packages the score-difference normalization used to state privacy directly in terms of +the range metric on score vectors. +-/ + +noncomputable section + +open scoped Classical + +namespace SLang +namespace PermuteAndFlip + +/-- +Coordinatewise score difference between two score vectors. +-/ +def scoreDiff {n : CandidateCount} (q q' : Scores n) : Fin n.succ → ℤ := + fun i => (q' i : ℤ) - q i + +namespace RangePrivacy + +def diffSet {n : CandidateCount} (q q' : Scores n) : Finset ℤ := + Finset.univ.image (scoreDiff q q') + +theorem diffSet_nonempty {n : CandidateCount} (q q' : Scores n) : (diffSet q q').Nonempty := by + exact ⟨scoreDiff q q' 0, Finset.mem_image.mpr ⟨0, by simp, rfl⟩⟩ + +def diffMin {n : CandidateCount} (q q' : Scores n) : ℤ := + (diffSet q q').min' (diffSet_nonempty q q') + +def diffMax {n : CandidateCount} (q q' : Scores n) : ℤ := + (diffSet q q').max' (diffSet_nonempty q q') + +/-- +The range distance on score vectors: the width of the set of coordinatewise score differences. + +Equivalently, this is `max_i (q' i - q i) - min_i (q' i - q i)`. +-/ +def rangeDistance {n : CandidateCount} (q q' : Scores n) : ℕ := + Int.toNat (diffMax q q' - diffMin q q') + +/-- +Shift amount that moves the minimum score difference to `0`. This is the +normalization that lets the privacy proof compare two natural-valued score +vectors without leaving `ℕ`. +-/ +def diffShift {n : CandidateCount} (q q' : Scores n) : ℕ := + Int.toNat (- diffMin q q') + +/-- The shifted coordinatewise differences, now normalized to lie in `[0, rangeDistance]`. -/ +def shiftedDiff {n : CandidateCount} (q q' : Scores n) : Fin n.succ → ℕ := + fun i => Int.toNat (scoreDiff q q' i + diffShift q q') + +/-- Lower endpoint of the normalized interval of score differences. -/ +def lowerEndpoint {n : CandidateCount} (q q' : Scores n) : ℕ := + Int.toNat (diffMin q q' + diffShift q q') + +/-- Upper endpoint of the normalized interval of score differences. -/ +def upperEndpoint {n : CandidateCount} (q q' : Scores n) : ℕ := + Int.toNat (diffMax q q' + diffShift q q') + +theorem scoreDiff_mem_interval + {n : CandidateCount} (q q' : Scores n) (i : Fin n.succ) : + diffMin q q' ≤ scoreDiff q q' i ∧ scoreDiff q q' i ≤ diffMax q q' := by + constructor + · exact Finset.min'_le _ _ (Finset.mem_image.mpr ⟨i, by simp, rfl⟩) + · exact Finset.le_max' _ _ (Finset.mem_image.mpr ⟨i, by simp, rfl⟩) + +theorem diffMin_add_diffShift_nonneg + {n : CandidateCount} (q q' : Scores n) : + 0 ≤ diffMin q q' + diffShift q q' := by + by_cases hmin : 0 ≤ diffMin q q' + · have hnonpos : -diffMin q q' ≤ 0 := by linarith + rw [diffShift, Int.toNat_of_nonpos hnonpos] + omega + · have hnonneg : 0 ≤ -diffMin q q' := by linarith + rw [diffShift, Int.toNat_of_nonneg hnonneg] + omega + +theorem shiftedDiff_eq_targetShift + {n : CandidateCount} (q q' : Scores n) : + (fun i => q i + shiftedDiff q q' i) = (fun i => q' i + diffShift q q') := by + funext i + have hmem := scoreDiff_mem_interval q q' i + have hnonneg : 0 ≤ scoreDiff q q' i + diffShift q q' := by + have hbase : 0 ≤ diffMin q q' + diffShift q q' := diffMin_add_diffShift_nonneg q q' + omega + have hcast : + ((q i + shiftedDiff q q' i : ℕ) : ℤ) = (q' i + diffShift q q' : ℕ) := by + dsimp [shiftedDiff] + rw [Int.toNat_of_nonneg hnonneg] + simp [scoreDiff] + omega + exact Int.ofNat.inj hcast + +/-! +The next three lemmas are the core normalization facts used in `Privacy.lean`: +every normalized coordinate lies between the common endpoints, and the width of +that interval is exactly the range distance. +-/ + +theorem lowerEndpoint_le_shiftedDiff + {n : CandidateCount} (q q' : Scores n) (i : Fin n.succ) : + lowerEndpoint q q' ≤ shiftedDiff q q' i := by + have hmem := scoreDiff_mem_interval q q' i + have _ : 0 ≤ diffMin q q' + diffShift q q' := diffMin_add_diffShift_nonneg q q' + have _ : 0 ≤ scoreDiff q q' i + diffShift q q' := by + omega + refine Int.toNat_le_toNat ?_ + omega + +theorem shiftedDiff_le_upperEndpoint + {n : CandidateCount} (q q' : Scores n) (i : Fin n.succ) : + shiftedDiff q q' i ≤ upperEndpoint q q' := by + have hmem := scoreDiff_mem_interval q q' i + have _ : 0 ≤ scoreDiff q q' i + diffShift q q' := by + have _ : 0 ≤ diffMin q q' + diffShift q q' := diffMin_add_diffShift_nonneg q q' + omega + refine Int.toNat_le_toNat ?_ + omega + +theorem upperEndpoint_eq_lowerEndpoint_add_rangeDistance + {n : CandidateCount} (q q' : Scores n) : + upperEndpoint q q' = lowerEndpoint q q' + rangeDistance q q' := by + have hleft_nonneg : 0 ≤ diffMin q q' + diffShift q q' := diffMin_add_diffShift_nonneg q q' + have hwidth_nonneg : 0 ≤ diffMax q q' - diffMin q q' := by + have hmem := scoreDiff_mem_interval q q' 0 + omega + have hsum_nonneg : 0 ≤ diffMax q q' + diffShift q q' := by + omega + apply Int.ofNat.inj + simp [upperEndpoint, lowerEndpoint, rangeDistance, + Int.toNat_of_nonneg hleft_nonneg, Int.toNat_of_nonneg hwidth_nonneg, + Int.toNat_of_nonneg hsum_nonneg] + omega + +end RangePrivacy + +abbrev rangeDistance {n : CandidateCount} (q q' : Scores n) : ℕ := + RangePrivacy.rangeDistance q q' + +end PermuteAndFlip +end SLang diff --git a/SampCert/DifferentialPrivacy/PermuteAndFlip/Reduction.lean b/SampCert/DifferentialPrivacy/PermuteAndFlip/Reduction.lean new file mode 100644 index 00000000..bf66308b --- /dev/null +++ b/SampCert/DifferentialPrivacy/PermuteAndFlip/Reduction.lean @@ -0,0 +1,268 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Shoemate +-/ +import Mathlib.Probability.ProbabilityMassFunction.Basic + +noncomputable section + +open scoped Classical + +namespace SLang +namespace PermuteAndFlip +namespace Reduction + +abbrev IntScores (n : ℕ) := Fin n.succ → ℤ +abbrev IntMechanism (n : ℕ) := IntScores n → PMF (Fin n.succ) + +def permuteScores {n : ℕ} (τ : Equiv.Perm (Fin n.succ)) (q : IntScores n) : IntScores n := + fun i => q (τ.symm i) + +def shiftScores {n : ℕ} (q : IntScores n) (c : ℤ) : IntScores n := + fun i => q i + c + +def raiseScore {n : ℕ} (q : IntScores n) (r : Fin n.succ) (k : ℤ) : IntScores n := + fun i => q i + if i = r then k else 0 + +def lowerScore {n : ℕ} (q : IntScores n) (r : Fin n.succ) (k : ℤ) : IntScores n := + raiseScore q r (-k) + +def Symmetric {n : ℕ} (M : IntMechanism n) : Prop := + ∀ (τ : Equiv.Perm (Fin n.succ)) (q : IntScores n) (r : Fin n.succ), + M (permuteScores τ q) (τ r) = M q r + +def ShiftInvariant {n : ℕ} (M : IntMechanism n) : Prop := + ∀ (q : IntScores n) (c : ℤ) (r : Fin n.succ), + M (shiftScores q c) r = M q r + +def Monotone {n : ℕ} (M : IntMechanism n) : Prop := + ∀ (q q' : IntScores n) (r : Fin n.succ), + q r ≤ q' r → + (∀ s : Fin n.succ, s ≠ r → q' s ≤ q s) → + M q r ≤ M q' r + +def Regular {n : ℕ} (M : IntMechanism n) : Prop := + Symmetric M ∧ ShiftInvariant M ∧ Monotone M + +def boundedPerturbation {n : ℕ} (δ : ℤ) (z : Fin n.succ → ℤ) : Prop := + ∀ i, -δ ≤ z i ∧ z i ≤ δ + +def boundedInterval {n : ℕ} (a b : ℤ) (z : Fin n.succ → ℤ) : Prop := + ∀ i, a ≤ z i ∧ z i ≤ b + +def scoreDiff {n : ℕ} (q q' : IntScores n) : Fin n.succ → ℤ := + fun i => q' i - q i + +def diffSet {n : ℕ} (q q' : IntScores n) : Finset ℤ := + Finset.univ.image (scoreDiff q q') + +theorem diffSet_nonempty {n : ℕ} (q q' : IntScores n) : (diffSet q q').Nonempty := by + have huniv : (Finset.univ : Finset (Fin n.succ)).Nonempty := ⟨0, by simp⟩ + rcases huniv with ⟨i, _hi⟩ + exact ⟨scoreDiff q q' i, Finset.mem_image.mpr ⟨i, by simp, rfl⟩⟩ + +def rangeDistance {n : ℕ} (q q' : IntScores n) : ℤ := + let s := diffSet q q' + s.max' (diffSet_nonempty q q') - s.min' (diffSet_nonempty q q') + +/-- +Abstract regularity-to-privacy reduction. + +This corresponds to the paper's Proposition 2: symmetry, shift-invariance, and +monotonicity reduce privacy to a single worst-case raise inequality on the +selected coordinate. +-/ +theorem reduced_privacy_of_regular + {n : ℕ} {M : IntMechanism n} {α : ENNReal} {δ : ℤ} + (Hreg : Regular M) + (Hred : ∀ (q : IntScores n) (r : Fin n.succ), + α * M (raiseScore q r (2 * δ)) r ≤ M q r) : + ∀ (q : IntScores n) (z : Fin n.succ → ℤ) (r : Fin n.succ), + boundedPerturbation δ z → + α * M q r ≤ M (fun i => q i + z i) r := by + intro q z r hz + rcases Hreg with ⟨_, Hshift, Hmono⟩ + have Hstep := Hred (lowerScore q r (2 * δ)) r + have hshiftScores : + shiftScores (lowerScore q r (2 * δ)) δ = + (fun i => q i + if i = r then (-δ) else δ) := by + funext i + by_cases hi : i = r + · subst hi + simp [lowerScore, raiseScore, shiftScores] + linarith + · simp [lowerScore, raiseScore, shiftScores, hi] + have Hshifted : + M (lowerScore q r (2 * δ)) r = + M (fun i => q i + if i = r then (-δ) else δ) r := by + rw [← Hshift (lowerScore q r (2 * δ)) δ r] + simp [hshiftScores] + have Hr : q r - δ ≤ q r + z r := by + have hz_r := hz r + simp at hz_r + linarith + have Hs : + ∀ s : Fin n.succ, s ≠ r → + q s + z s ≤ q s + if s = r then (-δ) else δ := by + intro s hs + have hz_s := hz s + simp [hs] at hz_s ⊢ + linarith + have Hr' : + (fun i => q i + if i = r then (-δ) else δ) r ≤ + (fun i => q i + z i) r := by + have hz_r := hz r + simp at hz_r ⊢ + linarith + have Hmono' := + Hmono + (fun i => q i + if i = r then (-δ) else δ) + (fun i => q i + z i) + r + Hr' + (by + intro s hs + have := Hs s hs + simpa [hs] using this) + have hraise : + raiseScore (lowerScore q r (2 * δ)) r (2 * δ) = q := by + funext i + by_cases hi : i = r + · subst hi + simp [lowerScore, raiseScore] + · simp [lowerScore, raiseScore, hi] + calc + α * M q r + = α * M (raiseScore (lowerScore q r (2 * δ)) r (2 * δ)) r := by + simp [hraise] + _ ≤ M (lowerScore q r (2 * δ)) r := Hstep + _ = M (fun i => q i + if i = r then (-δ) else δ) r := Hshifted + _ ≤ M (fun i => q i + z i) r := Hmono' + +/-- +Abstract interval version of the regularity reduction. + +This is the same reduction pattern as the paper's Proposition 2, but expressed +for an arbitrary interval `[a,b]` rather than the symmetric `[-δ, δ]` case. +-/ +theorem interval_privacy_of_regular + {n : ℕ} {M : IntMechanism n} {α : ENNReal} {a b : ℤ} + (Hreg : Regular M) + (Hred : ∀ (q : IntScores n) (r : Fin n.succ), + α * M (raiseScore q r (b - a)) r ≤ M q r) : + ∀ (q : IntScores n) (z : Fin n.succ → ℤ) (r : Fin n.succ), + boundedInterval a b z → + α * M q r ≤ M (fun i => q i + z i) r := by + intro q z r hz + rcases Hreg with ⟨_, Hshift, Hmono⟩ + have Hstep := Hred (lowerScore q r (b - a)) r + have hshiftScores : + shiftScores (lowerScore q r (b - a)) b = + (fun i => q i + if i = r then a else b) := by + funext i + by_cases hi : i = r + · subst hi + simp [lowerScore, raiseScore, shiftScores] + ring_nf + · simp [lowerScore, raiseScore, shiftScores, hi] + have Hshifted : + M (lowerScore q r (b - a)) r = + M (fun i => q i + if i = r then a else b) r := by + rw [← Hshift (lowerScore q r (b - a)) b r] + simp [hshiftScores] + have Hr' : + (fun i => q i + if i = r then a else b) r ≤ + (fun i => q i + z i) r := by + have hz_r := hz r + simp at hz_r ⊢ + linarith + have Hs : + ∀ s : Fin n.succ, s ≠ r → + q s + z s ≤ q s + if s = r then a else b := by + intro s hs + have hz_s := hz s + simp [hs] at hz_s ⊢ + linarith + have Hmono' := + Hmono + (fun i => q i + if i = r then a else b) + (fun i => q i + z i) + r + Hr' + (by + intro s hs + have := Hs s hs + simpa [hs] using this) + have hraise : + raiseScore (lowerScore q r (b - a)) r (b - a) = q := by + funext i + by_cases hi : i = r + · subst hi + simp [lowerScore, raiseScore] + ring + · simp [lowerScore, raiseScore, hi] + calc + α * M q r + = α * M (raiseScore (lowerScore q r (b - a)) r (b - a)) r := by + simp [hraise] + _ ≤ M (lowerScore q r (b - a)) r := Hstep + _ = M (fun i => q i + if i = r then a else b) r := Hshifted + _ ≤ M (fun i => q i + z i) r := Hmono' + +theorem boundedInterval_scoreDiff + {n : ℕ} (q q' : IntScores n) : + boundedInterval + ((diffSet q q').min' (diffSet_nonempty q q')) + ((diffSet q q').max' (diffSet_nonempty q q')) + (scoreDiff q q') := by + intro i + constructor + · exact Finset.min'_le _ _ (Finset.mem_image.mpr ⟨i, by simp, rfl⟩) + · exact Finset.le_max' _ _ (Finset.mem_image.mpr ⟨i, by simp, rfl⟩) + +theorem add_scoreDiff + {n : ℕ} (q q' : IntScores n) : + (fun i => q i + scoreDiff q q' i) = q' := by + funext i + simp [scoreDiff] + +/-- +Abstract privacy theorem stated directly in terms of range distance. + +This theorem is not stated in the paper in exactly this form; it is the +range-distance generalization of the same regularity reduction. +-/ +theorem range_privacy_of_regular + {n : ℕ} {M : IntMechanism n} {β : ℤ → ENNReal} + (Hreg : Regular M) + (Hred : ∀ (k : ℤ), 0 ≤ k → + ∀ (q : IntScores n) (r : Fin n.succ), + β k * M (raiseScore q r k) r ≤ M q r) : + ∀ (q q' : IntScores n) (r : Fin n.succ), + β (rangeDistance q q') * M q r ≤ M q' r := by + intro q q' r + let s : Finset ℤ := diffSet q q' + have hs : s.Nonempty := by simpa [s] using diffSet_nonempty q q' + let a : ℤ := s.min' hs + let b : ℤ := s.max' hs + have hab : 0 ≤ b - a := by + exact sub_nonneg.mpr (Finset.min'_le _ _ (Finset.max'_mem s hs)) + have hinterval := + interval_privacy_of_regular + (Hreg := Hreg) + (α := β (b - a)) + (a := a) + (b := b) + (Hred := Hred (b - a) hab) + (q := q) + (z := scoreDiff q q') + (r := r) + (boundedInterval_scoreDiff q q') + have hrange : rangeDistance q q' = b - a := by + simp [rangeDistance, s, a, b] + simpa [hrange, add_scoreDiff q q'] using hinterval + +end Reduction +end PermuteAndFlip +end SLang