cleaner definition of DP

SampCert/DiffPrivacy/BoundedAvg.lean

@@ -28,31 +28,18 @@ theorem NoisedBoundedAvgQueryIdentical (L U : ℤ) (h : L < U) (ε₁ ε₂ : 
   ext l x
   simp [NoisedBoundedAvgQuery, NoisedBoundedAvgQuery', PostProcess, Compose]
 
-theorem BoundedSumQueryDP (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedAvgQuery L U h ε₁ ε₂) ε₁ ε₂ := by
+theorem BoundedSumQueryDP (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedAvgQuery L U h ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
   rw [← NoisedBoundedAvgQueryIdentical]
   unfold NoisedBoundedAvgQuery'
   simp only
 
   have A := @NoisedCountingQueryDP ℤ ε₁ (2 * ε₂)
   have B := @NoisedBoundedSumQueryDP L U h ε₁ (2 * ε₂)
   have C := DPCompose B A
+  simp at C
+  ring_nf at C
+  rw [← division_def] at C
   have D := DPPostProcess C (fun z => z.1 / z.2)
-  simp [RAdd] at D
-
-  apply DP_cancel_sigma (ε₁ * (2 * ε₂) + 2 * ε₂ * ε₁) (2 * ε₂ * (2 * ε₂)) ε₁ ε₂ D
-  ring_nf
-  simp
-  ring_nf
-  rw [pow_two]
-  rw [← mul_assoc]
-  have A : (ε₂ : ℝ) ≠ 0 := by
-    simp
-  conv =>
-    left
-    left
-    rw [mul_assoc]
-    right
-    rw [mul_inv_cancel A]
-  simp
+  exact D
 
 end SLang

SampCert/DiffPrivacy/BoundedSum.lean

@@ -65,7 +65,7 @@ theorem BoundedSumQuerySensitivity (L U : ℤ) (h : L < U) : sensitivity (Bounde
 def NoisedBoundedSumQuery (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) (l : List ℤ) : SLang ℤ := do
   NoisedQuery (BoundedSumQuery L U) (maxBound L U h) ε₁ ε₂ l
 
-theorem NoisedBoundedSumQueryDP (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedSumQuery L U h ε₁ ε₂) ε₁ ε₂ := by
+theorem NoisedBoundedSumQueryDP (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedSumQuery L U h ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
   apply NoisedQueryDP
   apply BoundedSumQuerySensitivity
 

SampCert/DiffPrivacy/Count.lean

@@ -34,7 +34,7 @@ theorem CountingQuery1Sensitive :
 def NoisedCountingQuery (ε₁ ε₂ : ℕ+) (l : List T) : SLang ℤ := do
   NoisedQuery CountingQuery 1 ε₁ ε₂ l
 
-theorem NoisedCountingQueryDP (ε₁ ε₂ : ℕ+) : @DP T ℤ (NoisedCountingQuery ε₁ ε₂) ε₁ ε₂ := by
+theorem NoisedCountingQueryDP (ε₁ ε₂ : ℕ+) : @DP T ℤ (NoisedCountingQuery ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
   apply NoisedQueryDP
   apply CountingQuery1Sensitive
 

SampCert/DiffPrivacy/DP.lean

@@ -16,52 +16,20 @@ noncomputable section
 
 open Classical Nat Int Real
 
-def DP (q : List T → SLang U) (ε₁ ε₂ : ℕ+) : Prop :=
+def DP (q : List T → SLang U) (ε : ℝ) : Prop :=
   ∀ α : ℝ, 1 < α → ∀ l₁ l₂ : List T, Neighbour l₁ l₂ →
   RenyiDivergence
     (fun x : U => (q l₁ x).toReal)
     (fun x : U => (q l₂ x).toReal) α
-    ≤ (1/2) * (ε₁ / ε₂)^2 * α
-
-theorem DP_cancel_sigma {q : List T → SLang U} (ε₁ ε₂ ε₃ ε₄ : ℕ+) (h1 : DP q ε1 ε2) (h2 : @Eq.{1} Real
-  (@HDiv.hDiv.{0, 0, 0} Real Real Real
-    (@instHDiv.{0} Real
-      (@DivInvMonoid.toDiv.{0} Real
-        (@DivisionMonoid.toDivInvMonoid.{0} Real
-          (@DivisionCommMonoid.toDivisionMonoid.{0} Real
-            (@CommGroupWithZero.toDivisionCommMonoid.{0} Real
-              (@Semifield.toCommGroupWithZero.{0} Real
-                (@LinearOrderedSemifield.toSemifield.{0} Real
-                  (@LinearOrderedField.toLinearOrderedSemifield.{0} Real Real.instLinearOrderedField))))))))
-    (@Nat.cast.{0} Real Real.instNatCast (PNat.val ε1)) (@Nat.cast.{0} Real Real.instNatCast (PNat.val ε2)))
-  (@HDiv.hDiv.{0, 0, 0} Real Real Real
-    (@instHDiv.{0} Real
-      (@DivInvMonoid.toDiv.{0} Real
-        (@DivisionMonoid.toDivInvMonoid.{0} Real
-          (@DivisionCommMonoid.toDivisionMonoid.{0} Real
-            (@CommGroupWithZero.toDivisionCommMonoid.{0} Real
-              (@Semifield.toCommGroupWithZero.{0} Real
-                (@LinearOrderedSemifield.toSemifield.{0} Real
-                  (@LinearOrderedField.toLinearOrderedSemifield.{0} Real Real.instLinearOrderedField))))))))
-    (@Nat.cast.{0} Real Real.instNatCast (PNat.val ε3)) (@Nat.cast.{0} Real Real.instNatCast (PNat.val ε4)))) :
-  DP q ε3 ε4 := by
-  simp [DP] at *
-  intros α h3 l₁ l₂ h4
-  replace h1 := h1 α h3 l₁ l₂ h4
-  have A : (ε1 : ℝ) ^ 2 / ε2 ^ 2 = ε3 ^ 2 / ε4 ^ 2 := by
-    rw [← div_pow]
-    rw [← div_pow]
-    congr
-  rw [← A]
-  trivial
+    ≤ (1/2) * ε ^ 2 * α
 
 namespace SLang
 
 def NoisedQuery (query : List T → ℤ) (Δ : ℕ+) (ε₁ ε₂ : ℕ+) (l : List T) : SLang ℤ := do
   DiscreteGaussianGenSample (Δ * ε₂) ε₁ (query l)
 
 theorem NoisedQueryDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) :
-  DP (NoisedQuery query Δ ε₁ ε₂) ε₁ ε₂ := by
+  DP (NoisedQuery query Δ ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
   simp [DP, NoisedQuery]
   intros α h1 l₁ l₂ h2
   have A := @DiscreteGaussianGenSampleZeroConcentrated α h1 (Δ * ε₂) ε₁ (query l₁) (query l₂)
@@ -117,12 +85,9 @@ def Compose (nq1 nq2 : List T → SLang ℤ) (l : List T) : SLang (ℤ × ℤ) :
   let B ← nq2 l
   return (A,B)
 
-def RAdd (ε₁ ε₂ ε₃ ε₄ : ℕ+) : ℕ+ × ℕ+ :=
-  (ε₁ * ε₄ + ε₂ * ε₃,ε₂ * ε₄)
-
-theorem DPCompose {nq1 nq2 : List T → SLang ℤ} {ε₁ ε₂ ε₃ ε₄ : ℕ+} (h1 : DP nq1 ε₁ ε₂)  (h2 : DP nq2 ε₃ ε₄) :
-  DP (Compose nq1 nq2) (RAdd ε₁ ε₂ ε₃ ε₄).1 (RAdd ε₁ ε₂ ε₃ ε₄).2 := by
-  simp [Compose, RAdd, RenyiDivergence, DP]
+theorem DPCompose {nq1 nq2 : List T → SLang ℤ} {ε₁ ε₂ ε₃ ε₄ : ℕ+} (h1 : DP nq1 ((ε₁ : ℝ) / ε₂))  (h2 : DP nq2 ((ε₃ : ℝ) / ε₄)) :
+  DP (Compose nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by
+  simp [Compose, RenyiDivergence, DP]
   intro α h3 l₁ l₂ h4
   simp [DP] at h1 h2
   replace h1 := h1 α h3 l₁ l₂ h4
@@ -194,8 +159,8 @@ def PostProcess (nq : List T → SLang U) (pp : U → ℤ) (l : List T) : SLang
   let A ← nq l
   return pp A
 
-theorem DPPostProcess {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (h : DP nq ε₁ ε₂) (pp : U → ℤ)  :
-  DP (PostProcess nq pp) ε₁ ε₂ := by
+theorem DPPostProcess {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (h : DP nq ((ε₁ : ℝ) / ε₂)) (pp : U → ℤ)  :
+  DP (PostProcess nq pp) ((ε₁ : ℝ) / ε₂) := by
   simp [PostProcess, DP, RenyiDivergence]
   intro α h1 l₁ l₂ h2
   simp [DP, RenyiDivergence] at h